All Rewrite Rules

From Event-B
Jump to: navigation, search
CAUTION! Any modification to this page shall be announced on the User mailing list!

This page groups together all the rewrite rules implemented (or planned for implementation) in the Rodin prover. The rules themselves can be found in their respective location (for editing purposes):

Conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_rules

Set Rewrite Rules

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_SPECIAL_AND_BTRUE
<math> P \land \ldots \land \btrue \land \ldots \land Q \;\;\defi\;\; P \land \ldots \land Q </math> A
*
SIMP_SPECIAL_AND_BFALSE
<math> P \land \ldots \land \bfalse \land \ldots \land Q \;\;\defi\;\; \bfalse </math> A
*
SIMP_MULTI_AND
<math> P \land \ldots \land Q \land \ldots \land Q \land \ldots \land R \;\;\defi\;\; P \land \ldots \land Q \land \ldots \land R </math> A
*
SIMP_MULTI_AND_NOT
<math> P \land \ldots \land Q \land \ldots \land \lnot\, Q \land \ldots \land R \;\;\defi\;\; \bfalse </math> A
*
SIMP_SPECIAL_OR_BTRUE
<math> P \lor \ldots \lor \btrue \lor \ldots \lor Q \;\;\defi\;\; \btrue </math> A
*
SIMP_SPECIAL_OR_BFALSE
<math> P \lor \ldots \lor \bfalse \lor \ldots \lor Q \;\;\defi\;\; P \lor \ldots \lor Q </math> A
*
SIMP_MULTI_OR
<math> P \lor \ldots \lor Q \lor \ldots \lor Q \lor \ldots \lor R \;\;\defi\;\; P \lor \ldots \lor Q \lor \ldots \lor R </math> A
*
SIMP_MULTI_OR_NOT
<math> P \lor \ldots \lor Q \lor \ldots \lor \lnot\, Q \land \ldots \land R \;\;\defi\;\; \btrue </math> A
*
SIMP_SPECIAL_IMP_BTRUE_R
<math> P \limp \btrue \;\;\defi\;\; \btrue </math> A
*
SIMP_SPECIAL_IMP_BTRUE_L
<math> \btrue \limp P \;\;\defi\;\; P </math> A
*
SIMP_SPECIAL_IMP_BFALSE_R
<math> P \limp \bfalse \;\;\defi\;\; \lnot\, P </math> A
*
SIMP_SPECIAL_IMP_BFALSE_L
<math> \bfalse \limp P \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_IMP
<math> P \limp P \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_IMP_NOT_L
<math>\lnot P\limp P\;\;\defi\;\; P</math> A
*
SIMP_MULTI_IMP_NOT_R
<math>P\limp\lnot P\;\;\defi\;\;\lnot P</math> A
*
SIMP_MULTI_IMP_AND
<math> P \land \ldots \land Q \land \ldots \land R \limp Q \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_IMP_AND_NOT_R
<math> P \land \ldots \land Q \land \ldots \land R \limp \lnot\, Q \;\;\defi\;\; \lnot\,(P \land \ldots \land Q \land \ldots \land R) </math> A
*
SIMP_MULTI_IMP_AND_NOT_L
<math> P \land \ldots \land \lnot\, Q \land \ldots \land R \limp Q \;\;\defi\;\; \lnot\,(P \land \ldots \land \lnot\, Q \land \ldots \land R) </math> A
*
SIMP_MULTI_EQV
<math> P \leqv P \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_EQV_NOT
<math> P \leqv \lnot\, P \;\;\defi\;\; \bfalse </math> A
*
SIMP_SPECIAL_NOT_BTRUE
<math> \lnot\, \btrue \;\;\defi\;\; \bfalse </math> A
*
SIMP_SPECIAL_NOT_BFALSE
<math> \lnot\, \bfalse \;\;\defi\;\; \btrue </math> A
*
SIMP_NOT_NOT
<math> \lnot\, \lnot\, P \;\;\defi\;\; P </math> AM
*
SIMP_NOTEQUAL
<math> E \neq F \;\;\defi\;\; \lnot\, E = F </math> A
*
SIMP_NOTIN
<math> E \notin F \;\;\defi\;\; \lnot\, E \in F </math> A
*
SIMP_NOTSUBSET
<math> E \not\subset F \;\;\defi\;\; \lnot\, E \subset F </math> A
*
SIMP_NOTSUBSETEQ
<math> E \not\subseteq F \;\;\defi\;\; \lnot\, E \subseteq F </math> A
*
SIMP_NOT_LE
<math> \lnot\, a \leq b \;\;\defi\;\; a > b </math> A
*
SIMP_NOT_GE
<math> \lnot\, a \geq b \;\;\defi\;\; a < b </math> A
*
SIMP_NOT_LT
<math> \lnot\, a < b \;\;\defi\;\; a \geq b </math> A
*
SIMP_NOT_GT
<math> \lnot\, a > b \;\;\defi\;\; a \leq b </math> A
*
SIMP_SPECIAL_NOT_EQUAL_FALSE_R
<math> \lnot\, (E = \False ) \;\;\defi\;\; (E = \True ) </math> A
*
SIMP_SPECIAL_NOT_EQUAL_FALSE_L
<math> \lnot\, (\False = E) \;\;\defi\;\; (\True = E) </math> A
*
SIMP_SPECIAL_NOT_EQUAL_TRUE_R
<math> \lnot\, (E = \True ) \;\;\defi\;\; (E = \False ) </math> A
*
SIMP_SPECIAL_NOT_EQUAL_TRUE_L
<math> \lnot\, (\True = E) \;\;\defi\;\; (\False = E) </math> A
*
SIMP_FORALL_AND
<math> \forall x \qdot P \land Q \;\;\defi\;\; (\forall x \qdot P) \land (\forall x \qdot Q) </math> A
*
SIMP_EXISTS_OR
<math> \exists x \qdot P \lor Q \;\;\defi\;\; (\exists x \qdot P) \lor (\exists x \qdot Q) </math> A
*
SIMP_EXISTS_IMP
<math>\exists x\qdot P\limp Q\;\;\defi\;\;(\forall x\qdot P)\limp(\exists x\qdot Q)</math> A
*
SIMP_FORALL
<math> \forall \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \forall z \qdot P(z) </math> Quantified identifiers other than <math>z</math> do not occur in <math>P</math> A
*
SIMP_EXISTS
<math> \exists \ldots ,z,\ldots \qdot P(z) \;\;\defi\;\; \exists z \qdot P(z) </math> Quantified identifiers other than <math>z</math> do not occur in <math>P</math> A
*
SIMP_MULTI_EQUAL
<math> E = E \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_NOTEQUAL
<math> E \neq E \;\;\defi\;\; \bfalse </math> A
*
SIMP_EQUAL_MAPSTO
<math> E \mapsto F = G \mapsto H \;\;\defi\;\; E = G \land F = H </math> A
*
SIMP_EQUAL_SING
<math> \{ E\} = \{ F\} \;\;\defi\;\; E = F </math> A
*
SIMP_SPECIAL_EQUAL_TRUE
<math> \True = \False \;\;\defi\;\; \bfalse </math> A
*
SIMP_TYPE_SUBSETEQ
<math> S \subseteq \mathit{Ty} \;\;\defi\;\; \btrue </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_SUBSETEQ_SING
<math> \{ E\} \subseteq S \;\;\defi\;\; E \in S </math> where <math>E</math> is a single expression A
*
SIMP_SPECIAL_SUBSETEQ
<math> \emptyset \subseteq S \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_SUBSETEQ
<math> S \subseteq S \;\;\defi\;\; \btrue </math> A
*
SIMP_SUBSETEQ_BUNION
<math> S \subseteq A \bunion \ldots \bunion S \bunion \ldots \bunion B \;\;\defi\;\; \btrue </math> A
*
SIMP_SUBSETEQ_BINTER
<math> A \binter \ldots \binter S \binter \ldots \binter B \subseteq S \;\;\defi\;\; \btrue </math> A
*
DERIV_SUBSETEQ_BUNION
<math> A \bunion \ldots \bunion B \subseteq S \;\;\defi\;\; A \subseteq S \land \ldots \land B \subseteq S </math> A
*
DERIV_SUBSETEQ_BINTER
<math> S \subseteq A \binter \ldots \binter B \;\;\defi\;\; S \subseteq A \land \ldots \land S \subseteq B </math> A
*
SIMP_SPECIAL_IN
<math> E \in \emptyset \;\;\defi\;\; \bfalse </math> A
*
SIMP_MULTI_IN
<math> B \in \{ A, \ldots , B, \ldots , C\} \;\;\defi\;\; \btrue </math> A
*
SIMP_IN_SING
<math> E \in \{ F\} \;\;\defi\;\; E = F </math> A
*
SIMP_MULTI_SETENUM
<math> \{ A, \ldots , B, \ldots , B, \ldots , C\} \;\;\defi\;\; \{ A, \ldots , B, \ldots , C\} </math> A
*
SIMP_SPECIAL_BINTER
<math> S \binter \ldots \binter \emptyset \binter \ldots \binter T \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_BINTER
<math> S \binter \ldots \binter \mathit{Ty} \binter \ldots \binter T \;\;\defi\;\; S \binter \ldots \binter T </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_MULTI_BINTER
<math> S \binter \ldots \binter T \binter \ldots \binter T \binter \ldots \binter U \;\;\defi\;\; S \binter \ldots \binter T \binter \ldots \binter U </math> A
*
SIMP_MULTI_EQUAL_BINTER
<math> S \binter \ldots \binter T \binter \ldots \binter U = T \;\;\defi\;\; T \subseteq S \binter \ldots \binter U </math> A
*
SIMP_SPECIAL_BUNION
<math> S \bunion \ldots \bunion \emptyset \bunion \ldots \bunion T \;\;\defi\;\; S \bunion \ldots \bunion T </math> A
*
SIMP_TYPE_BUNION
<math> S \bunion \ldots \bunion \mathit{Ty} \bunion \ldots \bunion T \;\;\defi\;\; \mathit{Ty} </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_MULTI_BUNION
<math> S \bunion \ldots \bunion T \bunion \ldots \bunion T \bunion \ldots \bunion U \;\;\defi\;\; S \bunion \ldots \bunion T \bunion \ldots \bunion U </math> A
*
SIMP_MULTI_EQUAL_BUNION
<math> S \bunion \ldots \bunion T \bunion \ldots \bunion U = T \;\;\defi\;\; S \bunion \ldots \bunion U \subseteq T </math> A
*
SIMP_MULTI_SETMINUS
<math> S \setminus S \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_SETMINUS_R
<math> S \setminus \emptyset \;\;\defi\;\; S </math> A
*
SIMP_SPECIAL_SETMINUS_L
<math> \emptyset \setminus S \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_SETMINUS
<math> S \setminus \mathit{Ty} \;\;\defi\;\; \emptyset </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_TYPE_SETMINUS_SETMINUS
<math> \mathit{Ty} \setminus (\mathit{Ty} \setminus S) \;\;\defi\;\; S </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_KUNION_POW
<math> \union (\pow (S)) \;\;\defi\;\; S </math> A
*
SIMP_KUNION_POW1
<math> \union (\pown (S)) \;\;\defi\;\; S </math> A
*
SIMP_SPECIAL_KUNION
<math> \union (\{ \emptyset \} ) \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_QUNION
<math> \Union x\qdot \bfalse \mid E \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_KINTER
<math> \inter (\{ \emptyset \} ) \;\;\defi\;\; \emptyset </math> A
*
SIMP_KINTER_POW
<math> \inter (\pow (S)) \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_POW
<math> \pow (\emptyset ) \;\;\defi\;\; \{ \emptyset \} </math> A
*
SIMP_SPECIAL_POW1
<math> \pown (\emptyset ) \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_CPROD_R
<math> S \cprod \emptyset \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_CPROD_L
<math> \emptyset \cprod S \;\;\defi\;\; \emptyset </math> A
SIMP_COMPSET_EQUAL
<math> \{ x, y \qdot x = E(y) \land P(y) \mid F(x, y) \} \;\;\defi\;\; \{ y \qdot P(y) \mid F(E(y), y) \} </math> where <math>x</math> non free in <math>E</math> and non free in <math>P</math> A
*
SIMP_COMPSET_IN
<math> \{ x \qdot x \in S \mid x \} \;\;\defi\;\; S </math> where <math>x</math> non free in <math>S</math> A
*
SIMP_COMPSET_SUBSETEQ
<math> \{ x \qdot x \subseteq S \mid x \} \;\;\defi\;\; \pow (S) </math> where <math>x</math> non free in <math>S</math> A
*
SIMP_SPECIAL_COMPSET_BFALSE
<math> \{ x \qdot \bfalse \mid x \} \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_COMPSET_BTRUE
<math> \{ x \qdot \btrue \mid E \} \;\;\defi\;\; \mathit{Ty} </math> where the type of <math>E</math> is <math>\mathit{Ty}</math> and <math>E</math> is a maplet combination of locally-bound, pairwise-distinct bound identifiers A
*
SIMP_SUBSETEQ_COMPSET_L
<math> \{ x \qdot P(x) \mid E(x) \} \subseteq S \;\;\defi\;\; \forall y\qdot P(y) \limp E(y) \in S </math> where <math>y</math> is fresh A
*
SIMP_IN_COMPSET
<math> F \in \{ x,y,\ldots \qdot P(x,y,\ldots) \mid E(x,y,\ldots) \} \;\;\defi\;\; \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F </math> where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> A
*
SIMP_IN_COMPSET_ONEPOINT
<math> E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E) </math> Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate A
SIMP_SUBSETEQ_COMPSET_R
<math> S \subseteq \{ x \qdot P(x) \mid x \} \;\;\defi\;\; \forall y\qdot y \in S \limp P(y) </math> where <math>y</math> non free in <math>S, \{ x \qdot P(x) \mid x \}</math> M
*
SIMP_SPECIAL_OVERL
<math> r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s </math> A
*
SIMP_SPECIAL_KBOOL_BTRUE
<math> \bool (\btrue ) \;\;\defi\;\; \True </math> A
*
SIMP_SPECIAL_KBOOL_BFALSE
<math> \bool (\bfalse ) \;\;\defi\;\; \False </math> A
DISTRI_SUBSETEQ_BUNION_SING
<math> S \bunion \{ F\} \subseteq T \;\;\defi\;\; S \subseteq T \land F \in T </math> where <math>F</math> is a single expression M
*
DEF_FINITE
<math> \finite(S) \;\;\defi\;\; \exists n,f\qdot f\in 1\upto n \tbij S </math> M
*
SIMP_SPECIAL_FINITE
<math> \finite (\emptyset ) \;\;\defi\;\; \btrue </math> A
*
SIMP_FINITE_SETENUM
<math> \finite (\{ a, \ldots , b\} ) \;\;\defi\;\; \btrue </math> A
*
SIMP_FINITE_BUNION
<math> \finite (S \bunion T) \;\;\defi\;\; \finite (S) \land \finite (T) </math> A
SIMP_FINITE_UNION
<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp finite(x))</math> M
SIMP_FINITE_QUNION
<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp finite(E))</math> M
*
SIMP_FINITE_POW
<math> \finite (\pow (S)) \;\;\defi\;\; \finite (S) </math> A
*
DERIV_FINITE_CPROD
<math> \finite (S \cprod T) \;\;\defi\;\; S = \emptyset \lor T = \emptyset \lor (\finite (S) \land \finite (T)) </math> A
*
SIMP_FINITE_CONVERSE
<math> \finite (r^{-1} ) \;\;\defi\;\; \finite (r) </math> A
*
SIMP_FINITE_UPTO
<math> \finite (a \upto b) \;\;\defi\;\; \btrue </math> A
*
SIMP_FINITE_ID
<math> \finite (\id) \;\;\defi\;\; \finite (S) </math> where <math>\id</math> has type <math>\pow(S \cprod S)</math> A
*
SIMP_FINITE_ID_DOMRES
<math> \finite (E \domres \id) \;\;\defi\;\; \finite (E) </math> A
*
SIMP_FINITE_PRJ1
<math> \finite (\prjone) \;\;\defi\;\; \finite (S \cprod T) </math> where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> A
*
SIMP_FINITE_PRJ2
<math> \finite (\prjtwo) \;\;\defi\;\; \finite (S \cprod T) </math> where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> A
*
SIMP_FINITE_PRJ1_DOMRES
<math> \finite (E \domres \prjone) \;\;\defi\;\; \finite (E) </math> A
*
SIMP_FINITE_PRJ2_DOMRES
<math> \finite (E \domres \prjtwo) \;\;\defi\;\; \finite (E) </math> A
*
SIMP_FINITE_NATURAL
<math> \finite (\nat ) \;\;\defi\;\; \bfalse </math> A
*
SIMP_FINITE_NATURAL1
<math> \finite (\natn ) \;\;\defi\;\; \bfalse </math> A
*
SIMP_FINITE_INTEGER
<math> \finite (\intg ) \;\;\defi\;\; \bfalse </math> A
*
SIMP_FINITE_BOOL
<math> \finite (\Bool ) \;\;\defi\;\; \btrue </math> A
*
SIMP_FINITE_LAMBDA
<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{x\qdot P\mid E\} ) </math> where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> A
*
SIMP_TYPE_IN
<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_SPECIAL_EQV_BTRUE
<math> P \leqv \btrue \;\;\defi\;\; P </math> A
*
SIMP_SPECIAL_EQV_BFALSE
<math> P \leqv \bfalse \;\;\defi\;\; \lnot\, P </math> A
*
DEF_SUBSET
<math> A \subset B \;\;\defi\;\; A \subseteq B \land \lnot A = B </math> A
*
SIMP_SPECIAL_SUBSET_R
<math> S \subset \emptyset \;\;\defi\;\; \bfalse </math> A
*
SIMP_SPECIAL_SUBSET_L
<math>\emptyset\subset S \;\;\defi\;\; \lnot\; S = \emptyset</math> A
*
SIMP_TYPE_SUBSET_L
<math> S \subset \mathit{Ty} \;\;\defi\;\; S \neq \mathit{Ty} </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_MULTI_SUBSET
<math> S \subset S \;\;\defi\;\; \bfalse </math> A
*
SIMP_EQUAL_CONSTR
<math> \operatorname{constr} (a_1, \ldots, a_n) = \operatorname{constr} (b_1, \ldots, b_n) \;\;\defi\;\; a_1 = b_1 \land \ldots \land a_n = b_n </math> where <math>\operatorname{constr}</math> is a datatype constructor A
*
SIMP_EQUAL_CONSTR_DIFF
<math> \operatorname{constr_1} (\ldots) = \operatorname{constr_2} (\ldots) \;\;\defi\;\; \bfalse </math> where <math>\operatorname{constr_1}</math> and <math>\operatorname{constr_2}</math> are different datatype constructors A
*
SIMP_DESTR_CONSTR
<math> \operatorname{destr} (\operatorname{constr} (a_1, \ldots, a_n)) \;\;\defi\;\; a_i </math> where <math>\operatorname{destr}</math> is the datatype destructor for the i-th argument of datatype constructor <math>\operatorname{constr}</math> A
*
DISTRI_AND_OR
<math> P \land (Q \lor R) \;\;\defi\;\; (P \land Q) \lor (P \land R) </math> M
*
DISTRI_OR_AND
<math> P \lor (Q \land R) \;\;\defi\;\; (P \lor Q) \land (P \lor R) </math> M
*
DEF_OR
<math> P \lor Q \lor \ldots \lor R \;\;\defi\;\; \lnot\, P \limp (Q \lor \ldots \lor R) </math> M
*
DERIV_IMP
<math> P \limp Q \;\;\defi\;\; \lnot\, Q \limp \lnot\, P </math> M
*
DERIV_IMP_IMP
<math> P \limp (Q \limp R) \;\;\defi\;\; P \land Q \limp R </math> M
*
DISTRI_IMP_AND
<math> P \limp (Q \land R) \;\;\defi\;\; (P \limp Q) \land (P \limp R) </math> M
*
DISTRI_IMP_OR
<math> (P \lor Q) \limp R \;\;\defi\;\; (P \limp R) \land (Q \limp R) </math> M
*
DEF_EQV
<math> P \leqv Q \;\;\defi\;\; (P \limp Q) \land (Q \limp P) </math> M
*
DISTRI_NOT_AND
<math> \lnot\,(P \land Q) \;\;\defi\;\; \lnot\, P \lor \lnot\, Q </math> M
*
DISTRI_NOT_OR
<math> \lnot\,(P \lor Q) \;\;\defi\;\; \lnot\, P \land \lnot\, Q </math> M
*
DERIV_NOT_IMP
<math> \lnot\,(P \limp Q) \;\;\defi\;\; P \land \lnot\, Q </math> M
*
DERIV_NOT_FORALL
<math> \lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P </math> M
*
DERIV_NOT_EXISTS
<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math> M
*
DEF_IN_MAPSTO
<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math> AM
*
DEF_IN_POW
<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math> M
*
DEF_IN_POW1
<math> E \in \pown (S) \;\;\defi\;\; E \in \pow (S) \land S \neq \emptyset </math> M
*
DEF_SUBSETEQ
<math> S \subseteq T \;\;\defi\;\; \forall x \qdot x \in S \limp x \in T </math> where <math>x</math> is not free in <math>S</math> or <math>T</math> M
*
DEF_IN_BUNION
<math> E \in S \bunion T \;\;\defi\;\; E \in S \lor E \in T </math> M
*
DEF_IN_BINTER
<math> E \in S \binter T \;\;\defi\;\; E \in S \land E \in T </math> M
*
DEF_IN_SETMINUS
<math> E \in S \setminus T \;\;\defi\;\; E \in S \land \lnot\,(E \in T) </math> M
*
DEF_IN_SETENUM
<math> E \in \{ A, \ldots , B\} \;\;\defi\;\; E = A \lor \ldots \lor E = B </math> M
*
DEF_IN_KUNION
<math> E \in \union (S) \;\;\defi\;\; \exists s \qdot s \in S \land E \in s </math> where <math>s</math> is fresh M
*
DEF_IN_QUNION
<math> E \in (\Union x \qdot P(x) \mid T(x)) \;\;\defi\;\; \exists s \qdot P(s) \land E \in T(s) </math> where <math>s</math> is fresh M
*
DEF_IN_KINTER
<math> E \in \inter (S) \;\;\defi\;\; \forall s \qdot s \in S \limp E \in s </math> where <math>s</math> is fresh M
*
DEF_IN_QINTER
<math> E \in (\Inter x \qdot P(x) \mid T(x)) \;\;\defi\;\; \forall s \qdot P(s) \limp E \in T(s) </math> where <math>s</math> is fresh M
*
DEF_IN_UPTO
<math> E \in a \upto b \;\;\defi\;\; a \leq E \land E \leq b </math> M
*
DISTRI_BUNION_BINTER
<math> S \bunion (T \binter U) \;\;\defi\;\; (S \bunion T) \binter (S \bunion U) </math> M
*
DISTRI_BINTER_BUNION
<math> S \binter (T \bunion U) \;\;\defi\;\; (S \binter T) \bunion (S \binter U) </math> M
DISTRI_BINTER_SETMINUS
<math> S \binter (T \setminus U) \;\;\defi\;\; (S \binter T) \setminus (S \binter U) </math> M
DISTRI_SETMINUS_BUNION
<math> S \setminus (T \bunion U) \;\;\defi\;\; S \setminus T \setminus U </math> M
*
DERIV_TYPE_SETMINUS_BINTER
<math> \mathit{Ty} \setminus (S \binter T) \;\;\defi\;\; (\mathit{Ty} \setminus S) \bunion (\mathit{Ty} \setminus T) </math> where <math>\mathit{Ty}</math> is a type expression M
*
DERIV_TYPE_SETMINUS_BUNION
<math> \mathit{Ty} \setminus (S \bunion T) \;\;\defi\;\; (\mathit{Ty} \setminus S) \binter (\mathit{Ty} \setminus T) </math> where <math>\mathit{Ty}</math> is a type expression M
*
DERIV_TYPE_SETMINUS_SETMINUS
<math> \mathit{Ty} \setminus (S \setminus T) \;\;\defi\;\; (\mathit{Ty} \setminus S) \bunion T </math> where <math>\mathit{Ty}</math> is a type expression M
DISTRI_CPROD_BINTER
<math> S \cprod (T \binter U) \;\;\defi\;\; (S \cprod T) \binter (S \cprod U) </math> M
DISTRI_CPROD_BUNION
<math> S \cprod (T \bunion U) \;\;\defi\;\; (S \cprod T) \bunion (S \cprod U) </math> M
DISTRI_CPROD_SETMINUS
<math> S \cprod (T \setminus U) \;\;\defi\;\; (S \cprod T) \setminus (S \cprod U) </math> M
*
DERIV_SUBSETEQ
<math> S \subseteq T \;\;\defi\;\; (\mathit{Ty} \setminus T) \subseteq (\mathit{Ty} \setminus S) </math> where <math>\pow (\mathit{Ty})</math> is the type of <math>S</math> and <math>T</math> M
*
DERIV_EQUAL
<math> S = T \;\;\defi\;\; S \subseteq T \land T \subseteq S </math> where <math>\pow (\mathit{Ty})</math> is the type of <math>S</math> and <math>T</math> M
*
DERIV_SUBSETEQ_SETMINUS_L
<math> A \setminus B \subseteq S \;\;\defi\;\; A \subseteq B \bunion S </math> M
*
DERIV_SUBSETEQ_SETMINUS_R
<math> S \subseteq A \setminus B \;\;\defi\;\; S \subseteq A \land S \binter B = \emptyset </math> M
*
DEF_PARTITION
<math> \operatorname{partition} (s, s_1, s_2, \ldots, s_n) \;\;\defi\;\;
		  	\begin{array}{ll}

& s = s_1\bunion s_2\bunion\cdots\bunion s_n\\ \land& s_1\binter s_2 = \emptyset\\ \vdots\\ \land& s_1\binter s_n = \emptyset\\ \vdots\\ \land& s_{n-1}\binter s_n = \emptyset \end{array}</math>|| || AM

SIMP_EMPTY_PARTITION
<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math> A
SIMP_SINGLE_PARTITION
<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math> A

Relation Rewrite Rules

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
<math> \dom (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ x, \ldots , y\} </math> A
*
SIMP_DOM_CONVERSE
<math> \dom (r^{-1} ) \;\;\defi\;\; \ran (r) </math> A
*
SIMP_RAN_SETENUM
<math> \ran (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ a, \ldots , b\} </math> A
*
SIMP_RAN_CONVERSE
<math> \ran (r^{-1} ) \;\;\defi\;\; \dom (r) </math> A
*
SIMP_SPECIAL_OVERL
<math> r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s </math> A
*
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
*
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
*
SIMP_SPECIAL_DOMRES_L
<math> \emptyset \domres r \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_DOMRES_R
<math> S \domres \emptyset \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_DOMRES
<math> \mathit{Ty} \domres r \;\;\defi\;\; r </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_MULTI_DOMRES_DOM
<math> \dom (r) \domres r \;\;\defi\;\; r </math> A
*
SIMP_MULTI_DOMRES_RAN
<math> \ran (r) \domres r^{-1} \;\;\defi\;\; r^{-1} </math> A
*
SIMP_DOMRES_DOMRES_ID
<math> S \domres (T \domres \id) \;\;\defi\;\; (S \binter T) \domres \id </math> A
*
SIMP_DOMRES_DOMSUB_ID
<math> S \domres (T \domsub \id) \;\;\defi\;\; (S \setminus T) \domres \id </math> A
*
SIMP_SPECIAL_RANRES_R
<math> r \ranres \emptyset \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_RANRES_L
<math> \emptyset \ranres S \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_RANRES
<math> r \ranres \mathit{Ty} \;\;\defi\;\; r </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_MULTI_RANRES_RAN
<math> r \ranres \ran (r) \;\;\defi\;\; r </math> A
*
SIMP_MULTI_RANRES_DOM
<math> r^{-1} \ranres \dom (r) \;\;\defi\;\; r^{-1} </math> A
*
SIMP_RANRES_ID
<math> \id \ranres S \;\;\defi\;\; S \domres \id </math> A
*
SIMP_RANSUB_ID
<math> \id \ransub S \;\;\defi\;\; S \domsub \id </math> A
*
SIMP_RANRES_DOMRES_ID
<math> (S \domres \id) \ranres T \;\;\defi\;\; (S \binter T) \domres \id </math> A
*
SIMP_RANRES_DOMSUB_ID
<math> (S \domsub \id) \ranres T \;\;\defi\;\; (T \setminus S) \domres \id </math> A
*
SIMP_SPECIAL_DOMSUB_L
<math> \emptyset \domsub r \;\;\defi\;\; r </math> A
*
SIMP_SPECIAL_DOMSUB_R
<math> S \domsub \emptyset \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_DOMSUB
<math> \mathit{Ty} \domsub r \;\;\defi\;\; \emptyset </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_MULTI_DOMSUB_DOM
<math> \dom (r) \domsub r \;\;\defi\;\; \emptyset </math> A
*
SIMP_MULTI_DOMSUB_RAN
<math> \ran (r) \domsub r^{-1} \;\;\defi\;\; \emptyset </math> A
*
SIMP_DOMSUB_DOMRES_ID
<math> S \domsub (T \domres \id ) \;\;\defi\;\; (T \setminus S) \domres \id </math> A
*
SIMP_DOMSUB_DOMSUB_ID
<math> S \domsub (T \domsub \id ) \;\;\defi\;\; (S \bunion T) \domsub \id </math> A
*
SIMP_SPECIAL_RANSUB_R
<math> r \ransub \emptyset \;\;\defi\;\; r </math> A
*
SIMP_SPECIAL_RANSUB_L
<math> \emptyset \ransub S \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_RANSUB
<math> r \ransub \mathit{Ty} \;\;\defi\;\; \emptyset </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_MULTI_RANSUB_DOM
<math> r^{-1} \ransub \dom (r) \;\;\defi\;\; \emptyset </math> A
*
SIMP_MULTI_RANSUB_RAN
<math> r \ransub \ran (r) \;\;\defi\;\; \emptyset </math> A
*
SIMP_RANSUB_DOMRES_ID
<math> (S \domres \id) \ransub T \;\;\defi\;\; (S \setminus T) \domres \id </math> A
*
SIMP_RANSUB_DOMSUB_ID
<math> (S \domsub \id) \ransub T \;\;\defi\;\; (S \bunion T) \domsub \id </math> A
*
SIMP_SPECIAL_FCOMP
<math> r \fcomp \ldots \fcomp \emptyset \fcomp \ldots \fcomp s \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_FCOMP_ID
<math> r \fcomp \ldots \fcomp \id \fcomp \ldots \fcomp s \;\;\defi\;\; r \fcomp \ldots \fcomp s </math> A
*
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
*
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
*
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
*
SIMP_SPECIAL_BCOMP
<math> r \bcomp \ldots \bcomp \emptyset \bcomp \ldots \bcomp s \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_BCOMP_ID
<math> r \bcomp \ldots \bcomp \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp s </math> A
*
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
*
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
*
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
*
SIMP_SPECIAL_DPROD_R
<math> r \dprod \emptyset \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_DPROD_L
<math> \emptyset \dprod r \;\;\defi\;\; \emptyset </math> A
*
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
*
SIMP_SPECIAL_PPROD_R
<math> r \pprod \emptyset \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_PPROD_L
<math> \emptyset \pprod r \;\;\defi\;\; \emptyset </math> A
*
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
*
SIMP_SPECIAL_RELIMAGE_R
<math> r[\emptyset ] \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_RELIMAGE_L
<math> \emptyset [S] \;\;\defi\;\; \emptyset </math> A
*
SIMP_TYPE_RELIMAGE
<math> r[Ty] \;\;\defi\;\; \ran (r) </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_MULTI_RELIMAGE_DOM
<math> r[\dom (r)] \;\;\defi\;\; \ran (r) </math> A
*
SIMP_RELIMAGE_ID
<math> \id[T] \;\;\defi\;\; T </math> A
*
SIMP_RELIMAGE_DOMRES_ID
<math> (S \domres \id)[T] \;\;\defi\;\; S \binter T </math> A
*
SIMP_RELIMAGE_DOMSUB_ID
<math> (S \domsub \id)[T] \;\;\defi\;\; T \setminus S </math> A
*
SIMP_MULTI_RELIMAGE_CPROD_SING
<math> (\{ E\} \cprod S)[\{ E\} ] \;\;\defi\;\; S </math> where <math>E</math> is a single expression A
*
SIMP_MULTI_RELIMAGE_SING_MAPSTO
<math> \{ E \mapsto F\} [\{ E\} ] \;\;\defi\;\; \{ F\} </math> where <math>E</math> is a single expression A
*
SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB
<math> (r \ransub S)^{-1} [S] \;\;\defi\;\; \emptyset </math> A
*
SIMP_MULTI_RELIMAGE_CONVERSE_RANRES
<math> (r \ranres S)^{-1} [S] \;\;\defi\;\; r^{-1} [S] </math> A
*
SIMP_RELIMAGE_CONVERSE_DOMSUB
<math> (S \domsub r)^{-1} [T] \;\;\defi\;\; r^{-1} [T] \setminus S </math> A
DERIV_RELIMAGE_RANSUB
<math> (r \ransub S)[T] \;\;\defi\;\; r[T] \setminus S </math> M
DERIV_RELIMAGE_RANRES
<math> (r \ranres S)[T] \;\;\defi\;\; r[T] \binter S </math> M
*
SIMP_MULTI_RELIMAGE_DOMSUB
<math> (S \domsub r)[S] \;\;\defi\;\; \emptyset </math> A
DERIV_RELIMAGE_DOMSUB
<math> (S \domsub r)[T] \;\;\defi\;\; r[T \setminus S] </math> M
DERIV_RELIMAGE_DOMRES
<math> (S \domres r)[T] \;\;\defi\;\; r[S \binter T] </math> M
*
SIMP_SPECIAL_CONVERSE
<math> \emptyset ^{-1} \;\;\defi\;\; \emptyset </math> A
*
SIMP_CONVERSE_ID
<math> \id^{-1} \;\;\defi\;\; \id </math> A
*
SIMP_CONVERSE_CPROD
<math> (\mathit{S} \cprod \mathit{T})^{-1} \;\;\defi\;\; \mathit{T} \cprod \mathit{S} </math> A
*
SIMP_CONVERSE_SETENUM
<math> \{ x \mapsto a, \ldots , y \mapsto b\} ^{-1} \;\;\defi\;\; \{ a \mapsto x, \ldots , b \mapsto y\} </math> A
*
SIMP_CONVERSE_COMPSET
<math> \{ X \qdot P \mid x\mapsto y\} ^{-1} \;\;\defi\;\; \{ X \qdot P \mid y\mapsto x\} </math> A
*
SIMP_DOM_ID
<math> \dom (\id) \;\;\defi\;\; S </math> where <math>\id</math> has type <math>\pow(S \cprod S)</math> A
*
SIMP_RAN_ID
<math> \ran (\id) \;\;\defi\;\; S </math> where <math>\id</math> has type <math>\pow(S \cprod S)</math> A
*
SIMP_FCOMP_ID_L
<math> (S \domres \id) \fcomp r \;\;\defi\;\; S \domres r </math> A
*
SIMP_FCOMP_ID_R
<math> r \fcomp (S \domres \id) \;\;\defi\;\; r \ranres S </math> A
*
SIMP_SPECIAL_REL_R
<math> S \rel \emptyset \;\;\defi\;\; \{ \emptyset \} </math> idem for operators <math>\srel \pfun \pinj \psur</math> A
*
SIMP_SPECIAL_REL_L
<math> \emptyset \rel S \;\;\defi\;\; \{ \emptyset \} </math> idem for operators <math>\trel \pfun \tfun \pinj \tinj</math> A
*
SIMP_FUNIMAGE_PRJ1
<math> \prjone (E \mapsto F) \;\;\defi\;\; E </math> A
*
SIMP_FUNIMAGE_PRJ2
<math> \prjtwo (E \mapsto F) \;\;\defi\;\; F </math> A
*
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
*
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
*
SIMP_RAN_PRJ1
<math> \ran (\prjone) \;\;\defi\;\; S </math> where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> A
*
SIMP_RAN_PRJ2
<math> \ran (\prjtwo) \;\;\defi\;\; T </math> where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> A
*
SIMP_FUNIMAGE_LAMBDA
<math> (\lambda x \qdot P(x) \mid E(x))(y) \;\;\defi\;\; E(y) </math> A
*
SIMP_DOM_LAMBDA
<math>\dom(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid E\}</math> A
*
SIMP_RAN_LAMBDA
<math>\ran(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid F\} </math> A
*
SIMP_IN_FUNIMAGE
<math>E\mapsto F(E)\in F \;\;\defi\;\; \btrue</math> A
*
SIMP_IN_FUNIMAGE_CONVERSE_L
<math>F^{-1}(E)\mapsto E\in F \;\;\defi\;\; \btrue</math> A
*
SIMP_IN_FUNIMAGE_CONVERSE_R
<math>F(E)\mapsto E\in F^{-1} \;\;\defi\;\; \btrue</math> A
*
SIMP_MULTI_FUNIMAGE_SETENUM_LL
<math> \{ A \mapsto E, \ldots , B \mapsto E\} (x) \;\;\defi\;\; E </math> A
*
SIMP_MULTI_FUNIMAGE_SETENUM_LR
<math> \{ E, \ldots , x \mapsto y, \ldots , F\} (x) \;\;\defi\;\; y </math> A
*
SIMP_MULTI_FUNIMAGE_OVERL_SETENUM
<math> (r \ovl \ldots \ovl \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y </math> A
*
SIMP_MULTI_FUNIMAGE_BUNION_SETENUM
<math> (r \bunion \ldots \bunion \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y </math> A
*
SIMP_FUNIMAGE_CPROD
<math> (S \cprod \{ F\} )(x) \;\;\defi\;\; F </math> A
*
SIMP_FUNIMAGE_ID
<math> \id (x) \;\;\defi\;\; x </math> A
*
SIMP_FUNIMAGE_FUNIMAGE_CONVERSE
<math> f(f^{-1} (E)) \;\;\defi\;\; E </math> A
*
SIMP_FUNIMAGE_CONVERSE_FUNIMAGE
<math> f^{-1}(f(E)) \;\;\defi\;\; E </math> A
*
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
*
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
*
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
*
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
*
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
*
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
DEF_BCOMP
<math> r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r </math> M
DERIV_ID_SING
<math> \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} </math> where <math>E</math> is a single expression M
*
SIMP_SPECIAL_DOM
<math> \dom (\emptyset ) \;\;\defi\;\; \emptyset </math> A
*
SIMP_SPECIAL_RAN
<math> \ran (\emptyset ) \;\;\defi\;\; \emptyset </math> A
*
SIMP_CONVERSE_CONVERSE
<math> r^{-1-1} \;\;\defi\;\; r </math> A
*
DERIV_RELIMAGE_FCOMP
<math> (p \fcomp q)[s] \;\;\defi\;\; q[p[s]] </math> M
*
DERIV_FCOMP_DOMRES
<math> (s \domres p) \fcomp q \;\;\defi\;\; s \domres (p \fcomp q) </math> M
*
DERIV_FCOMP_DOMSUB
<math> (s \domsub p) \fcomp q \;\;\defi\;\; s \domsub (p \fcomp q) </math> M
*
DERIV_FCOMP_RANRES
<math> p \fcomp (q \ranres s) \;\;\defi\;\; (p \fcomp q) \ranres s </math> M
*
DERIV_FCOMP_RANSUB
<math> p \fcomp (q \ransub s) \;\;\defi\;\; (p \fcomp q) \ransub s </math> M
DERIV_FCOMP_SING
<math> \{E\mapsto F\}\fcomp\{F\mapsto G\} \;\;\defi\;\; \{E\mapsto G\} </math> A
*
SIMP_SPECIAL_EQUAL_RELDOMRAN
<math> \emptyset \strel \emptyset \;\;\defi\;\; \{ \emptyset \} </math> idem for operators <math>\tsur \tbij</math> A
*
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
*
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
*
SIMP_MULTI_DOM_CPROD
<math> \dom (E \cprod E) \;\;\defi\;\; E </math> A
*
SIMP_MULTI_RAN_CPROD
<math> \ran (E \cprod E) \;\;\defi\;\; E </math> A
*
SIMP_MULTI_DOM_DOMRES
<math>\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A</math> A
*
SIMP_MULTI_DOM_DOMSUB
<math>\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A</math> A
*
SIMP_MULTI_RAN_RANRES
<math>\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A</math> A
*
SIMP_MULTI_RAN_RANSUB
<math>\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A</math> A
*
DEF_IN_DOM
<math> E \in \dom (r) \;\;\defi\;\; \exists y \qdot E \mapsto y \in r </math> M
*
DEF_IN_RAN
<math> F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r </math> M
*
DEF_IN_CONVERSE
<math> E \mapsto F \in r^{-1} \;\;\defi\;\; F \mapsto E \in r </math> M
*
DEF_IN_DOMRES
<math> E \mapsto F \in S \domres r \;\;\defi\;\; E \in S \land E \mapsto F \in r </math> M
*
DEF_IN_RANRES
<math> E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \in T </math> M
*
DEF_IN_DOMSUB
<math> E \mapsto F \in S \domsub r \;\;\defi\;\; E \notin S \land E \mapsto F \in r </math> M
*
DEF_IN_RANSUB
<math> E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \notin T </math> M
*
DEF_IN_RELIMAGE
<math> F \in r[w] \;\;\defi\;\; \exists x \qdot x \in w \land x \mapsto F \in r </math> M
*
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
*
DEF_OVERL
<math> p \ovl q \;\;\defi\;\; (\dom (q) \domsub p) \bunion q </math> M
*
DEF_IN_ID
<math> E \mapsto F \in \id \;\;\defi\;\; E = F </math> M
*
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
*
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
*
DEF_IN_REL
<math> r \in S \rel T \;\;\defi\;\; r\subseteq S\cprod T</math> M
*
DEF_IN_RELDOM
<math> r \in S \trel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S </math> M
*
DEF_IN_RELRAN
<math> r \in S \srel T \;\;\defi\;\; r \in S \rel T \land \ran (r) = T </math> M
*
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
*
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
*
DEF_IN_TFCT
<math> f \in S \tfun T \;\;\defi\;\; f \in S \pfun T \land \dom (f) = S </math> M
*
DEF_IN_INJ
<math> f \in S \pinj T \;\;\defi\;\; f \in S \pfun T \land f^{-1} \in T \pfun S </math> M
*
DEF_IN_TINJ
<math> f \in S \tinj T \;\;\defi\;\; f \in S \pinj T \land \dom (f) = S </math> M
*
DEF_IN_SURJ
<math> f \in S \psur T \;\;\defi\;\; f \in S \pfun T \land \ran (f) = T </math> M
*
DEF_IN_TSURJ
<math> f \in S \tsur T \;\;\defi\;\; f \in S \psur T \land \dom (f) = S </math> M
*
DEF_IN_BIJ
<math> f \in S \tbij T \;\;\defi\;\; f \in S \tinj T \land \ran (f) = T </math> M
DISTRI_BCOMP_BUNION
<math> r \bcomp (s \bunion t) \;\;\defi\;\; (r \bcomp s) \bunion (r \bcomp t) </math> M
*
DISTRI_FCOMP_BUNION_R
<math> p \fcomp (q \bunion r) \;\;\defi\;\; (p \fcomp q) \bunion (p \fcomp r) </math> M
*
DISTRI_FCOMP_BUNION_L
<math> (q \bunion r) \fcomp p \;\;\defi\;\; (q \fcomp p) \bunion (r \fcomp p) </math> M
DISTRI_DPROD_BUNION
<math> r \dprod (s \bunion t) \;\;\defi\;\; (r \dprod s) \bunion (r \dprod t) </math> M
DISTRI_DPROD_BINTER
<math> r \dprod (s \binter t) \;\;\defi\;\; (r \dprod s) \binter (r \dprod t) </math> M
DISTRI_DPROD_SETMINUS
<math> r \dprod (s \setminus t) \;\;\defi\;\; (r \dprod s) \setminus (r \dprod t) </math> M
DISTRI_DPROD_OVERL
<math> r \dprod (s \ovl t) \;\;\defi\;\; (r \dprod s) \ovl (r \dprod t) </math> M
DISTRI_PPROD_BUNION
<math> r \pprod (s \bunion t) \;\;\defi\;\; (r \pprod s) \bunion (r \pprod t) </math> M
DISTRI_PPROD_BINTER
<math> r \pprod (s \binter t) \;\;\defi\;\; (r \pprod s) \binter (r \pprod t) </math> M
DISTRI_PPROD_SETMINUS
<math> r \pprod (s \setminus t) \;\;\defi\;\; (r \pprod s) \setminus (r \pprod t) </math> M
DISTRI_PPROD_OVERL
<math> r \pprod (s \ovl t) \;\;\defi\;\; (r \pprod s) \ovl (r \pprod t) </math> M
DISTRI_OVERL_BUNION_L
<math> (p \bunion q) \ovl r \;\;\defi\;\; (p \ovl r) \bunion (q \ovl r) </math> M
DISTRI_OVERL_BINTER_L
<math> (p \binter q) \ovl r \;\;\defi\;\; (p \ovl r) \binter (q \ovl r) </math> M
*
DISTRI_DOMRES_BUNION_R
<math> s \domres (p \bunion q) \;\;\defi\;\; (s \domres p) \bunion (s \domres q) </math> M
*
DISTRI_DOMRES_BUNION_L
<math> (s \bunion t) \domres r \;\;\defi\;\; (s \domres r) \bunion (t \domres r) </math> M
*
DISTRI_DOMRES_BINTER_R
<math> s \domres (p \binter q) \;\;\defi\;\; (s \domres p) \binter (s \domres q) </math> M
*
DISTRI_DOMRES_BINTER_L
<math> (s \binter t) \domres r \;\;\defi\;\; (s \domres r) \binter (t \domres r) </math> M
DISTRI_DOMRES_SETMINUS_R
<math> s \domres (p \setminus q) \;\;\defi\;\; (s \domres p) \setminus (s \domres q) </math> M
DISTRI_DOMRES_SETMINUS_L
<math> (s \setminus t) \domres r \;\;\defi\;\; (s \domres r) \setminus (t \domres r) </math> M
DISTRI_DOMRES_DPROD
<math> s \domres (p \dprod q) \;\;\defi\;\; (s \domres p) \dprod (s \domres q) </math> M
DISTRI_DOMRES_OVERL
<math> s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (s \domres q) </math> M
*
DISTRI_DOMSUB_BUNION_R
<math> s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q) </math> M
*
DISTRI_DOMSUB_BUNION_L
<math> (s \bunion t) \domsub r \;\;\defi\;\; (s \domsub r) \binter (t \domsub r) </math> M
*
DISTRI_DOMSUB_BINTER_R
<math> s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q) </math> M
*
DISTRI_DOMSUB_BINTER_L
<math> (s \binter t) \domsub r \;\;\defi\;\; (s \domsub r) \bunion (t \domsub r) </math> M
DISTRI_DOMSUB_DPROD
<math> A \domsub (r \dprod s) \;\;\defi\;\; (A \domsub r) \dprod (A \domsub s) </math> M
DISTRI_DOMSUB_OVERL
<math> A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s) </math> M
*
DISTRI_RANRES_BUNION_R
<math> r \ranres (s \bunion t) \;\;\defi\;\; (r \ranres s) \bunion (r \ranres t) </math> M
*
DISTRI_RANRES_BUNION_L
<math> (p \bunion q) \ranres s \;\;\defi\;\; (p \ranres s) \bunion (q \ranres s) </math> M
*
DISTRI_RANRES_BINTER_R
<math> r \ranres (s \binter t) \;\;\defi\;\; (r \ranres s) \binter (r \ranres t) </math> M
*
DISTRI_RANRES_BINTER_L
<math> (p \binter q) \ranres s \;\;\defi\;\; (p \ranres s) \binter (q \ranres s) </math> M
DISTRI_RANRES_SETMINUS_R
<math> r \ranres (s \setminus t) \;\;\defi\;\; (r \ranres s) \setminus (r \ranres t) </math> M
DISTRI_RANRES_SETMINUS_L
<math> (p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s) </math> M
*
DISTRI_RANSUB_BUNION_R
<math> r \ransub (s\bunion t) \;\;\defi\;\; (r \ransub s) \binter (r \ransub t) </math> M
*
DISTRI_RANSUB_BUNION_L
<math> (p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s) </math> M
*
DISTRI_RANSUB_BINTER_R
<math> r \ransub (s \binter t) \;\;\defi\;\; (r \ransub s) \bunion (r \ransub t) </math> M
*
DISTRI_RANSUB_BINTER_L
<math> (p \binter q) \ransub s \;\;\defi\;\; (p \ransub s) \binter (q \ransub s) </math> M
*
DISTRI_CONVERSE_BUNION
<math> (p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1} </math> M
DISTRI_CONVERSE_BINTER
<math> (p \binter q)^{-1} \;\;\defi\;\; p^{-1} \binter q^{-1} </math> M
DISTRI_CONVERSE_SETMINUS
<math> (r \setminus s)^{-1} \;\;\defi\;\; r^{-1} \setminus s^{-1} </math> M
DISTRI_CONVERSE_BCOMP
<math> (r \bcomp s)^{-1} \;\;\defi\;\; (s^{-1} \bcomp r^{-1} ) </math> M
DISTRI_CONVERSE_FCOMP
<math> (p \fcomp q)^{-1} \;\;\defi\;\; (q^{-1} \fcomp p^{-1} ) </math> M
DISTRI_CONVERSE_PPROD
<math> (r \pprod s)^{-1} \;\;\defi\;\; r^{-1} \pprod s^{-1} </math> M
DISTRI_CONVERSE_DOMRES
<math> (s \domres r)^{-1} \;\;\defi\;\; r^{-1} \ranres s </math> M
DISTRI_CONVERSE_DOMSUB
<math> (s \domsub r)^{-1} \;\;\defi\;\; r^{-1} \ransub s </math> M
DISTRI_CONVERSE_RANRES
<math> (r \ranres s)^{-1} \;\;\defi\;\; s \domres r^{-1} </math> M
DISTRI_CONVERSE_RANSUB
<math> (r \ransub s)^{-1} \;\;\defi\;\; s \domsub r^{-1} </math> M
*
DISTRI_DOM_BUNION
<math> \dom (r \bunion s) \;\;\defi\;\; \dom (r) \bunion \dom (s) </math> M
*
DISTRI_RAN_BUNION
<math> \ran (r \bunion s) \;\;\defi\;\; \ran (r) \bunion \ran (s) </math> M
*
DISTRI_RELIMAGE_BUNION_R
<math> r[S \bunion T] \;\;\defi\;\; r[S] \bunion r[T] </math> M
*
DISTRI_RELIMAGE_BUNION_L
<math> (p \bunion q)[S] \;\;\defi\;\; p[S] \bunion q[S] </math> M
*
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
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
*
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
*
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
*
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
*
SIMP_MAPSTO_PRJ1_PRJ2
<math>\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E </math> A
DERIV_EXPAND_PRJS
<math> E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E) </math> M
*
SIMP_DOM_SUCC
<math>\dom(\usucc) \;\;\defi\;\; \intg</math> A
*
SIMP_RAN_SUCC
<math>\ran(\usucc) \;\;\defi\;\; \intg</math> A
*
DERIV_MULTI_IN_BUNION
<math> E\in A\bunion\cdots\bunion\left\{\cdots, E,\cdots\right\}\bunion\cdots\bunion B\;\;\defi\;\; \btrue</math> A
*
DERIV_MULTI_IN_SETMINUS
<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> A
*
DEF_PRED
<math> \upred\;\;\defi\;\; \usucc^{-1}</math> A

Empty Set Rewrite Rules

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.

All rewrite rules that match the pattern <math>\textbf{P}=\emptyset</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\emptyset</math> and <math>\emptyset=\textbf{P}</math>, as these predicates are equivalent. All rewrite rules that match the pattern <math>\textbf{P}=\mathit{Ty}</math> are also applicable to predicates of the form <math>\mathit{Ty}\subseteq\textbf{P}</math> and <math>\mathit{Ty}=\textbf{P}</math>, as these predicates are equivalent.


  Name Rule Side Condition A/M
*
DEF_SPECIAL_NOT_EQUAL
<math> \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S </math> where <math>x</math> is not free in <math>S</math> M
*
SIMP_SETENUM_EQUAL_EMPTY
<math> \{ A, \ldots , B\} = \emptyset \;\;\defi\;\; \bfalse </math> A
*
SIMP_SPECIAL_EQUAL_COMPSET
<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math> A
*
SIMP_BINTER_EQUAL_TYPE
<math> A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \cdots \land B = \mathit{Ty} </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_BINTER_SING_EQUAL_EMPTY
<math>A\binter\cdots\binter\{a\}\binter\cdots\binter B = \emptyset \;\;\defi\;\; \lnot\, a \in A\binter\cdots\binter B</math> A
*
SIMP_BINTER_SETMINUS_EQUAL_EMPTY
<math>A\binter\cdots\binter(B\setminus C)\binter\cdots\binter D = \emptyset \;\;\defi\;\; (A\binter\cdots\binter B\binter\cdots\binter D) \setminus C = \emptyset</math> A
*
SIMP_BUNION_EQUAL_EMPTY
<math> A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \cdots \land B = \emptyset </math> A
*
SIMP_SETMINUS_EQUAL_EMPTY
<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math> A
*
SIMP_SETMINUS_EQUAL_TYPE
<math> A \setminus B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land B = \emptyset </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_POW_EQUAL_EMPTY
<math> \pow (S) = \emptyset \;\;\defi\;\; \bfalse </math> A
*
SIMP_POW1_EQUAL_EMPTY
<math> \pown (S) = \emptyset \;\;\defi\;\; S = \emptyset </math> A
*
SIMP_KINTER_EQUAL_TYPE
<math> \inter (S) = \mathit{Ty} \;\;\defi\;\; S = \{ \mathit{Ty} \} </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_KUNION_EQUAL_EMPTY
<math> \union (S) = \emptyset \;\;\defi\;\; S \subseteq \{ \emptyset \} </math> A
*
SIMP_QINTER_EQUAL_TYPE
<math> (\Inter x\qdot P(x) \mid E(x)) = \mathit{Ty} \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \mathit{Ty}</math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_QUNION_EQUAL_EMPTY
<math> (\Union x\qdot P(x) \mid E(x)) = \emptyset \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \emptyset</math> A
*
SIMP_NATURAL_EQUAL_EMPTY
<math> \nat = \emptyset \;\;\defi\;\; \bfalse</math> A
*
SIMP_NATURAL1_EQUAL_EMPTY
<math> \natn = \emptyset \;\;\defi\;\; \bfalse</math> A
*
SIMP_TYPE_EQUAL_EMPTY
<math> \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_CPROD_EQUAL_EMPTY
<math> S \cprod T = \emptyset \;\;\defi\;\; S = \emptyset \lor T = \emptyset </math> A
*
SIMP_CPROD_EQUAL_TYPE
<math> S \cprod T = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land T = \mathit{Tb} </math> where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> A
*
SIMP_UPTO_EQUAL_EMPTY
<math> i \upto j = \emptyset \;\;\defi\;\; i > j </math> A
*
SIMP_UPTO_EQUAL_INTEGER
<math> i \upto j = \intg \;\;\defi\;\; \bfalse </math> A
*
SIMP_UPTO_EQUAL_NATURAL
<math> i \upto j = \nat \;\;\defi\;\; \bfalse </math> A
*
SIMP_UPTO_EQUAL_NATURAL1
<math> i \upto j = \natn \;\;\defi\;\; \bfalse </math> A
*
SIMP_SPECIAL_EQUAL_REL
<math> A \rel B = \emptyset \;\;\defi\;\; \bfalse </math> idem for operators <math>\pfun \pinj</math> A
SIMP_TYPE_EQUAL_REL
<math> A \rel B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ta} \land B = \mathit{Tb} </math> where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> A
*
SIMP_SPECIAL_EQUAL_RELDOM
<math> A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset </math> idem for operator <math>\tfun</math> A
SIMP_TYPE_EQUAL_RELDOMRAN
<math> A \trel B = \mathit{Ty} \;\;\defi\;\; \bfalse </math> where <math>\mathit{Ty}</math> is a type expression, idem for operator <math>\srel, \strel, \tfun, \tinj, \psur, \tsur, \tbij</math> A
*
SIMP_SREL_EQUAL_EMPTY
<math> A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset </math> A
*
SIMP_STREL_EQUAL_EMPTY
<math> A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) </math> A
*
SIMP_DOM_EQUAL_EMPTY
<math> \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset </math> A
*
SIMP_RAN_EQUAL_EMPTY
<math> \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset </math> A
*
SIMP_FCOMP_EQUAL_EMPTY
<math> p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset </math> A
*
SIMP_BCOMP_EQUAL_EMPTY
<math> p \bcomp q = \emptyset \;\;\defi\;\; \ran (q) \binter \dom (p) = \emptyset </math> A
*
SIMP_DOMRES_EQUAL_EMPTY
<math> S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset </math> A
*
SIMP_DOMRES_EQUAL_TYPE
<math> S \domres r = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land r = \mathit{Ty} </math> where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> A
*
SIMP_DOMSUB_EQUAL_EMPTY
<math> S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S </math> A
*
SIMP_DOMSUB_EQUAL_TYPE
<math> S \domsub r = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty} </math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_RANRES_EQUAL_EMPTY
<math> r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset</math> A
*
SIMP_RANRES_EQUAL_TYPE
<math> r \ranres S = \mathit{Ty} \;\;\defi\;\; S = \mathit{Tb} \land r = \mathit{Ty}</math> where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> A
*
SIMP_RANSUB_EQUAL_EMPTY
<math> r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S </math> A
*
SIMP_RANSUB_EQUAL_TYPE
<math> r \ransub S = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty}</math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_CONVERSE_EQUAL_EMPTY
<math> r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset</math> A
*
SIMP_CONVERSE_EQUAL_TYPE
<math> r^{-1} = \mathit{Ty} \;\;\defi\;\; r = \mathit{Ty}^{-1}</math> where <math>\mathit{Ty}</math> is a type expression A
*
SIMP_RELIMAGE_EQUAL_EMPTY
<math> r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset</math> A
*
SIMP_OVERL_EQUAL_EMPTY
<math> r \ovl \cdots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \cdots \land s = \emptyset </math> A
*
SIMP_DPROD_EQUAL_EMPTY
<math> p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset </math> A
*
SIMP_DPROD_EQUAL_TYPE
<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math> where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> A
*
SIMP_PPROD_EQUAL_EMPTY
<math> p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math> A
*
SIMP_PPROD_EQUAL_TYPE
<math> p \pprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tc} \land q = \mathit{Tb} \cprod \mathit{Td} </math> where <math>\mathit{Ty}</math> is a type expression equal to <math>(\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td})</math> A
*
SIMP_ID_EQUAL_EMPTY
<math> \id = \emptyset \;\;\defi\;\; \bfalse </math> A
*
SIMP_PRJ1_EQUAL_EMPTY
<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math> A
*
SIMP_PRJ2_EQUAL_EMPTY
<math> \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math> A

Arithmetic Rewrite Rules

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_SPECIAL_MOD_0
<math> 0 \,\bmod\, E \;\;\defi\;\; 0 </math> A
*
SIMP_SPECIAL_MOD_1
<math> E \,\bmod\, 1 \;\;\defi\;\; 0 </math> A
*
SIMP_MIN_SING
<math> \min (\{ E\} ) \;\;\defi\;\; E </math> where <math>E</math> is a single expression A
*
SIMP_MAX_SING
<math> \max (\{ E\} ) \;\;\defi\;\; E </math> where <math>E</math> is a single expression A
*
SIMP_MIN_NATURAL
<math> \min (\nat ) \;\;\defi\;\; 0 </math> A
*
SIMP_MIN_NATURAL1
<math> \min (\natn ) \;\;\defi\;\; 1 </math> A
*
SIMP_MIN_BUNION_SING
<math> \begin{array}{cl} & \min (S \bunion \ldots \bunion \{ \min (T)\} \bunion \ldots \bunion U) \\ \defi & \min (S \bunion \ldots \bunion T \bunion \ldots \bunion U) \\ \end{array} </math> A
*
SIMP_MAX_BUNION_SING
<math> \begin{array}{cl} & \max (S \bunion \ldots \bunion \{ \max (T)\} \bunion \ldots \bunion U) \\ \defi & \max (S \bunion \ldots \bunion T \bunion \ldots \bunion U) \\ \end{array} </math> A
*
SIMP_MIN_UPTO
<math> \min (E \upto F) \;\;\defi\;\; E </math> A
*
SIMP_MAX_UPTO
<math> \max (E \upto F) \;\;\defi\;\; F </math> A
*
SIMP_LIT_MIN
<math> \min (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \min (\{ E, \ldots , i, \ldots , H\} ) </math> where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> A
*
SIMP_LIT_MAX
<math> \max (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \max (\{ E, \ldots , i, \ldots , H\} ) </math> where <math>i</math> and <math>j</math> are literals and <math>i \geq j</math> A
*
SIMP_SPECIAL_CARD
<math> \card (\emptyset ) \;\;\defi\;\; 0 </math> A
*
SIMP_CARD_SING
<math> \card (\{ E\} ) \;\;\defi\;\; 1 </math> where <math>E</math> is a single expression A
*
SIMP_SPECIAL_EQUAL_CARD
<math> \card (S) = 0 \;\;\defi\;\; S = \emptyset </math> A
*
SIMP_CARD_POW
<math> \card (\pow (S)) \;\;\defi\;\; 2\expn{\card(S)} </math> A
*
SIMP_CARD_BUNION
<math> \card (S \bunion T) \;\;\defi\;\; \card (S) + \card (T) - \card (S \binter T) </math> A
SIMP_CARD_SETMINUS
<math>\card(S\setminus T)\;\;\defi\;\;\card(S) - \card(T)</math> with hypotheses <math>T\subseteq S</math> and either <math>\finite(S)</math> or <math>\finite(T)</math> A
SIMP_CARD_SETMINUS_SETENUM
<math>\card(S\setminus\{E_1,\ldots,E_n\})\;\;\defi\;\;\card(S) - \card(\{E_1,\ldots,E_n\})</math> with hypotheses <math>E_i\in S</math> for all <math>i\in 1\upto n</math> A
*
SIMP_CARD_CONVERSE
<math> \card (r^{-1} ) \;\;\defi\;\; \card (r) </math> A
*
SIMP_CARD_ID
<math> \card (\id) \;\;\defi\;\; \card (S) </math> where <math>\id</math> has type <math>\pow (S \cprod S) </math> A
*
SIMP_CARD_ID_DOMRES
<math> \card (S\domres\id) \;\;\defi\;\; \card (S) </math> A
*
SIMP_CARD_PRJ1
<math> \card (\prjone) \;\;\defi\;\; \card (S \cprod T) </math> where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> A
*
SIMP_CARD_PRJ2
<math> \card (\prjtwo) \;\;\defi\;\; \card (S \cprod T) </math> where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> A
*
SIMP_CARD_PRJ1_DOMRES
<math> \card (E \domres \prjone) \;\;\defi\;\; \card (E) </math> A
*
SIMP_CARD_PRJ2_DOMRES
<math> \card (E \domres \prjtwo) \;\;\defi\;\; \card (E) </math> A
*
SIMP_CARD_LAMBDA
<math> \card(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \card(\{x\qdot P\mid E\} ) </math> where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> A
*
SIMP_LIT_CARD_UPTO
<math> \card (i \upto j) \;\;\defi\;\; j-i+1 </math> where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> A
SIMP_TYPE_CARD
<math> \card (\mathit{Tenum}) \;\;\defi\;\; N </math> where <math>\mathit{Tenum}</math> is a carrier set containing <math>N</math> elements A
*
SIMP_LIT_GE_CARD_1
<math> \card (S) \geq 1 \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_LE_CARD_1
<math> 1 \leq \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_LE_CARD_0
<math> 0 \leq \card (S) \;\;\defi\;\; \btrue </math> A
*
SIMP_LIT_GE_CARD_0
<math> \card (S) \geq 0 \;\;\defi\;\; \btrue </math> A
*
SIMP_LIT_GT_CARD_0
<math> \card (S) > 0 \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_LT_CARD_0
<math> 0 < \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_EQUAL_CARD_1
<math> \card (S) = 1 \;\;\defi\;\; \exists x \qdot S = \{ x\} </math> A
*
SIMP_CARD_NATURAL
<math> \card (S) \in \nat \;\;\defi\;\; \btrue </math> A
*
SIMP_CARD_NATURAL1
<math> \card (S) \in \natn \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_IN_NATURAL
<math> i \in \nat \;\;\defi\;\; \btrue </math> where <math>i</math> is a non-negative literal A
*
SIMP_SPECIAL_IN_NATURAL1
<math> 0 \in \natn \;\;\defi\;\; \bfalse </math> A
*
SIMP_LIT_IN_NATURAL1
<math> i \in \natn \;\;\defi\;\; \btrue </math> where <math>i</math> is a positive literal A
*
SIMP_LIT_UPTO
<math> i \upto j \;\;\defi\;\; \emptyset </math> where <math>i</math> and <math>j</math> are literals and <math>j < i</math> A
*
SIMP_LIT_IN_MINUS_NATURAL
<math> -i \in \nat \;\;\defi\;\; \bfalse </math> where <math>i</math> is a positive literal A
*
SIMP_LIT_IN_MINUS_NATURAL1
<math> -i \in \natn \;\;\defi\;\; \bfalse </math> where <math>i</math> is a non-negative literal A
*
DEF_IN_NATURAL
<math>x \in \nat \;\;\defi\;\; 0 \leq x </math> M
*
DEF_IN_NATURAL1
<math>x \in \natn \;\;\defi\;\; 1 \leq x </math> M
*
SIMP_LIT_EQUAL_KBOOL_TRUE
<math> \bool (P) = \True \;\;\defi\;\; P </math> A
*
SIMP_LIT_EQUAL_KBOOL_FALSE
<math> \bool (P) = \False \;\;\defi\;\; \lnot\, P </math> A
DEF_EQUAL_MIN
<math> E = \min (S) \;\;\defi\;\; E \in S \land (\forall x \qdot x \in S \limp E \leq x) </math> where <math>x</math> non free in <math>S, E</math> M
DEF_EQUAL_MAX
<math> E = \max (S) \;\;\defi\;\; E \in S \land (\forall x \qdot x \in S \limp E \geq x) </math> where <math>x</math> non free in <math>S, E</math> M
*
SIMP_SPECIAL_PLUS
<math> E + \ldots + 0 + \ldots + F \;\;\defi\;\; E + \ldots + F </math> A
*
SIMP_SPECIAL_MINUS_R
<math> E - 0 \;\;\defi\;\; E </math> A
*
SIMP_SPECIAL_MINUS_L
<math> 0 - E \;\;\defi\;\; -E </math> A
*
SIMP_MINUS_MINUS
<math> - (- E) \;\;\defi\;\; E </math> A
*
SIMP_MINUS_UNMINUS
<math> E - (- F) \;\;\defi\;\; E + F </math> where <math>(-F)</math> is a unary minus expression or a negative literal M
*
SIMP_MULTI_MINUS
<math> E - E \;\;\defi\;\; 0 </math> A
*
SIMP_MULTI_MINUS_PLUS_L
<math> (A + \ldots + C + \ldots + B) - C \;\;\defi\;\; A + \ldots + B </math> M
*
SIMP_MULTI_MINUS_PLUS_R
<math> C - (A + \ldots + C + \ldots + B) \;\;\defi\;\; -(A + \ldots + B) </math> M
*
SIMP_MULTI_MINUS_PLUS_PLUS
<math> (A + \ldots + E + \ldots + B) - (C + \ldots + E + \ldots + D) \;\;\defi\;\; (A + \ldots + B) - (C + \ldots + D) </math> M
*
SIMP_MULTI_PLUS_MINUS
<math>(A + \ldots + D + \ldots + (C - D) + \ldots + B) \;\;\defi\;\; A + \ldots + C + \ldots + B </math> M
*
SIMP_MULTI_ARITHREL_PLUS_PLUS
<math> A + \ldots + E + \ldots + B < C + \ldots + E + \ldots + D \;\;\defi\;\; A + \ldots + B < C + \ldots + D </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_MULTI_ARITHREL_PLUS_R
<math> C < A + \ldots + C \ldots + B \;\;\defi\;\; 0 < A + \ldots + B </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_MULTI_ARITHREL_PLUS_L
<math> A + \ldots + C \ldots + B < C \;\;\defi\;\; A + \ldots + B < 0 </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_MULTI_ARITHREL_MINUS_MINUS_R
<math> A - C < B - C \;\;\defi\;\; A < B </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_MULTI_ARITHREL_MINUS_MINUS_L
<math> C - A < C - B \;\;\defi\;\; B < A </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_SPECIAL_PROD_0
<math> E * \ldots * 0 * \ldots * F \;\;\defi\;\; 0 </math> A
*
SIMP_SPECIAL_PROD_1
<math> E * \ldots * 1 * \ldots * F \;\;\defi\;\; E * \ldots * F </math> A
*
SIMP_SPECIAL_PROD_MINUS_EVEN
<math> (-E) * \ldots * (-F) \;\;\defi\;\; E * \ldots * F </math> if an even number of <math>-</math> A
*
SIMP_SPECIAL_PROD_MINUS_ODD
<math> (-E) * \ldots * (-F) \;\;\defi\;\; -(E * \ldots * F) </math> if an odd number of <math>-</math> A
*
SIMP_LIT_MINUS
<math> - (i) \;\;\defi\;\; (-i) </math> where <math>i</math> is a literal A
*
SIMP_LIT_EQUAL
<math> i = j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_LIT_LE
<math> i \leq j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_LIT_LT
<math> i < j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_LIT_GE
<math> i \geq j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_LIT_GT
<math> i > j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_DIV_MINUS
<math> (- E) \div (-F) \;\;\defi\;\; E \div F </math> A
*
SIMP_SPECIAL_DIV_1
<math> E \div 1 \;\;\defi\;\; E </math> A
*
SIMP_SPECIAL_DIV_0
<math> 0 \div E \;\;\defi\;\; 0 </math> A
*
SIMP_SPECIAL_EXPN_1_R
<math> E ^ 1 \;\;\defi\;\; E </math> A
*
SIMP_SPECIAL_EXPN_1_L
<math> 1 ^ E \;\;\defi\;\; 1 </math> A
*
SIMP_SPECIAL_EXPN_0
<math> E ^ 0 \;\;\defi\;\; 1 </math> A
*
SIMP_MULTI_LE
<math> E \leq E \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_LT
<math> E < E \;\;\defi\;\; \bfalse </math> A
*
SIMP_MULTI_GE
<math> E \geq E \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_GT
<math> E > E \;\;\defi\;\; \bfalse </math> A
*
SIMP_MULTI_DIV
<math> E \div E \;\;\defi\;\; 1 </math> A
*
SIMP_MULTI_DIV_PROD
<math> (X * \ldots * E * \ldots * Y) \div E \;\;\defi\;\; X * \ldots * Y </math> A
*
SIMP_MULTI_MOD
<math> E \,\bmod\, E \;\;\defi\;\; 0 </math> A
DISTRI_PROD_PLUS
<math> a * (b + c) \;\;\defi\;\; (a * b) + (a * c) </math> M
DISTRI_PROD_MINUS
<math> a * (b - c) \;\;\defi\;\; (a * b) - (a * c) </math> M
DERIV_NOT_EQUAL
<math> \lnot E = F \;\;\defi\;\; E < F \lor E > F </math> <math>E</math> and <math>F</math> must be of Integer type M

Extension Proof Rules

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.

Rewrite Rules

  Name Rule Side Condition A/M
*
SIMP_SPECIAL_COND_BTRUE
<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math> A
*
SIMP_SPECIAL_COND_BFALSE
<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math> A
*
SIMP_MULTI_COND
<math> \operatorname{COND}(C, E, E) \;\;\defi\;\; E </math> A


Inference Rules

  Name Rule Side Condition A/M
*
DATATYPE_DISTINCT_CASE
<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math> where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers M


*
DATATYPE_INDUCTION
<math>\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math> where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}</math> are the inductive parameters (if any); an antecedent is created for every constructor <math>c_i</math> of <math>DT</math>; all parameters are introduced as fresh identifiers; examples here M