All Rewrite Rules

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

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	$\dom (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ x, \ldots , y\}$		A
*	SIMP_DOM_CONVERSE	$\dom (r^{-1} ) \;\;\defi\;\; \ran (r)$		A
*	SIMP_RAN_SETENUM	$\ran (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ a, \ldots , b\}$		A
*	SIMP_RAN_CONVERSE	$\ran (r^{-1} ) \;\;\defi\;\; \dom (r)$		A
*	SIMP_SPECIAL_OVERL	$r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s$		A
*	SIMP_MULTI_OVERL	$r_1 \ovl \cdots \ovl r_n \defi r_1 \ovl \cdots \ovl r_{i-1} \ovl r_{i+1} \ovl \cdots \ovl r_n$	there is a $j$ such that $1\leq i < j \leq n$ and $r_i$ and $r_j$ are syntactically equal.	A
*	SIMP_TYPE_OVERL_CPROD	$r\ovl\cdots\ovl\mathit{Ty}\ovl\cdots\ovl s \;\defi\;\; \mathit{Ty}\ovl\cdots\ovl s$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_SPECIAL_DOMRES_L	$\emptyset \domres r \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_DOMRES_R	$S \domres \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_DOMRES	$\mathit{Ty} \domres r \;\;\defi\;\; r$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_DOMRES_DOM	$\dom (r) \domres r \;\;\defi\;\; r$		A
*	SIMP_MULTI_DOMRES_RAN	$\ran (r) \domres r^{-1} \;\;\defi\;\; r^{-1}$		A
*	SIMP_DOMRES_DOMRES_ID	$S \domres (T \domres \id) \;\;\defi\;\; (S \binter T) \domres \id$		A
*	SIMP_DOMRES_DOMSUB_ID	$S \domres (T \domsub \id) \;\;\defi\;\; (S \setminus T) \domres \id$		A
*	SIMP_SPECIAL_RANRES_R	$r \ranres \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RANRES_L	$\emptyset \ranres S \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RANRES	$r \ranres \mathit{Ty} \;\;\defi\;\; r$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_RANRES_RAN	$r \ranres \ran (r) \;\;\defi\;\; r$		A
*	SIMP_MULTI_RANRES_DOM	$r^{-1} \ranres \dom (r) \;\;\defi\;\; r^{-1}$		A
*	SIMP_RANRES_ID	$\id \ranres S \;\;\defi\;\; S \domres \id$		A
*	SIMP_RANSUB_ID	$\id \ransub S \;\;\defi\;\; S \domsub \id$		A
*	SIMP_RANRES_DOMRES_ID	$(S \domres \id) \ranres T \;\;\defi\;\; (S \binter T) \domres \id$		A
*	SIMP_RANRES_DOMSUB_ID	$(S \domsub \id) \ranres T \;\;\defi\;\; (T \setminus S) \domres \id$		A
*	SIMP_SPECIAL_DOMSUB_L	$\emptyset \domsub r \;\;\defi\;\; r$		A
*	SIMP_SPECIAL_DOMSUB_R	$S \domsub \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_DOMSUB	$\mathit{Ty} \domsub r \;\;\defi\;\; \emptyset$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_DOMSUB_DOM	$\dom (r) \domsub r \;\;\defi\;\; \emptyset$		A
*	SIMP_MULTI_DOMSUB_RAN	$\ran (r) \domsub r^{-1} \;\;\defi\;\; \emptyset$		A
*	SIMP_DOMSUB_DOMRES_ID	$S \domsub (T \domres \id ) \;\;\defi\;\; (T \setminus S) \domres \id$		A
*	SIMP_DOMSUB_DOMSUB_ID	$S \domsub (T \domsub \id ) \;\;\defi\;\; (S \bunion T) \domsub \id$		A
*	SIMP_SPECIAL_RANSUB_R	$r \ransub \emptyset \;\;\defi\;\; r$		A
*	SIMP_SPECIAL_RANSUB_L	$\emptyset \ransub S \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RANSUB	$r \ransub \mathit{Ty} \;\;\defi\;\; \emptyset$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_RANSUB_DOM	$r^{-1} \ransub \dom (r) \;\;\defi\;\; \emptyset$		A
*	SIMP_MULTI_RANSUB_RAN	$r \ransub \ran (r) \;\;\defi\;\; \emptyset$		A
*	SIMP_RANSUB_DOMRES_ID	$(S \domres \id) \ransub T \;\;\defi\;\; (S \setminus T) \domres \id$		A
*	SIMP_RANSUB_DOMSUB_ID	$(S \domsub \id) \ransub T \;\;\defi\;\; (S \bunion T) \domsub \id$		A
*	SIMP_SPECIAL_FCOMP	$r \fcomp \ldots \fcomp \emptyset \fcomp \ldots \fcomp s \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_FCOMP_ID	$r \fcomp \ldots \fcomp \id \fcomp \ldots \fcomp s \;\;\defi\;\; r \fcomp \ldots \fcomp s$		A
*	SIMP_TYPE_FCOMP_R	$r \fcomp \mathit{Ty} \;\;\defi\;\; \dom (r) \cprod \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_FCOMP_L	$\mathit{Ty} \fcomp r \;\;\defi\;\; \mathit{Ta} \cprod \ran (r)$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_FCOMP_ID	$r \fcomp \ldots \fcomp S \domres \id \fcomp T \domres \id \fcomp \ldots s \;\;\defi\;\; r \fcomp \ldots \fcomp (S \binter T) \domres \id \fcomp \ldots \fcomp s$		A
*	SIMP_SPECIAL_BCOMP	$r \bcomp \ldots \bcomp \emptyset \bcomp \ldots \bcomp s \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_BCOMP_ID	$r \bcomp \ldots \bcomp \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp s$		A
*	SIMP_TYPE_BCOMP_L	$\mathit{Ty} \bcomp r \;\;\defi\;\; \dom (r) \cprod \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_BCOMP_R	$r \bcomp \mathit{Ty} \;\;\defi\;\; \mathit{Ta} \cprod \ran (r)$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_BCOMP_ID	$r \bcomp \ldots \bcomp S \domres \id \bcomp T \domres \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp (S \binter T) \domres \id \bcomp \ldots \bcomp s$		A
*	SIMP_SPECIAL_DPROD_R	$r \dprod \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_DPROD_L	$\emptyset \dprod r \;\;\defi\;\; \emptyset$		A
*	SIMP_DPROD_CPROD	$(\mathit{S} \cprod \mathit{T}) \dprod (\mathit{U} \cprod \mathit{V}) \;\;\defi\;\; \mathit{S} \binter \mathit{U} \cprod (\mathit{T} \cprod \mathit{V})$		A
*	SIMP_SPECIAL_PPROD_R	$r \pprod \emptyset \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_PPROD_L	$\emptyset \pprod r \;\;\defi\;\; \emptyset$		A
*	SIMP_PPROD_CPROD	$(\mathit{S} \cprod \mathit{T}) \pprod (\mathit{U} \cprod \mathit{V}) \;\;\defi\;\; (\mathit{S} \cprod \mathit{U}) \cprod (\mathit{T} \cprod \mathit{V})$		A
*	SIMP_SPECIAL_RELIMAGE_R	$r[\emptyset ] \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RELIMAGE_L	$\emptyset [S] \;\;\defi\;\; \emptyset$		A
*	SIMP_TYPE_RELIMAGE	$r[Ty] \;\;\defi\;\; \ran (r)$	where $\mathit{Ty}$ is a type expression	A
*	SIMP_MULTI_RELIMAGE_DOM	$r[\dom (r)] \;\;\defi\;\; \ran (r)$		A
*	SIMP_RELIMAGE_ID	$\id[T] \;\;\defi\;\; T$		A
*	SIMP_RELIMAGE_DOMRES_ID	$(S \domres \id)[T] \;\;\defi\;\; S \binter T$		A
*	SIMP_RELIMAGE_DOMSUB_ID	$(S \domsub \id)[T] \;\;\defi\;\; T \setminus S$		A
*	SIMP_MULTI_RELIMAGE_CPROD_SING	$(\{ E\} \cprod S)[\{ E\} ] \;\;\defi\;\; S$	where $E$ is a single expression	A
*	SIMP_MULTI_RELIMAGE_SING_MAPSTO	$\{ E \mapsto F\} [\{ E\} ] \;\;\defi\;\; \{ F\}$	where $E$ is a single expression	A
*	SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB	$(r \ransub S)^{-1} [S] \;\;\defi\;\; \emptyset$		A
*	SIMP_MULTI_RELIMAGE_CONVERSE_RANRES	$(r \ranres S)^{-1} [S] \;\;\defi\;\; r^{-1} [S]$		A
*	SIMP_RELIMAGE_CONVERSE_DOMSUB	$(S \domsub r)^{-1} [T] \;\;\defi\;\; r^{-1} [T] \setminus S$		A
	DERIV_RELIMAGE_RANSUB	$(r \ransub S)[T] \;\;\defi\;\; r[T] \setminus S$		M
	DERIV_RELIMAGE_RANRES	$(r \ranres S)[T] \;\;\defi\;\; r[T] \binter S$		M
*	SIMP_MULTI_RELIMAGE_DOMSUB	$(S \domsub r)[S] \;\;\defi\;\; \emptyset$		A
	DERIV_RELIMAGE_DOMSUB	$(S \domsub r)[T] \;\;\defi\;\; r[T \setminus S]$		M
	DERIV_RELIMAGE_DOMRES	$(S \domres r)[T] \;\;\defi\;\; r[S \binter T]$		M
*	SIMP_SPECIAL_CONVERSE	$\emptyset ^{-1} \;\;\defi\;\; \emptyset$		A
*	SIMP_CONVERSE_ID	$\id^{-1} \;\;\defi\;\; \id$		A
*	SIMP_CONVERSE_CPROD	$(\mathit{S} \cprod \mathit{T})^{-1} \;\;\defi\;\; \mathit{T} \cprod \mathit{S}$		A
*	SIMP_CONVERSE_SETENUM	$\{ x \mapsto a, \ldots , y \mapsto b\} ^{-1} \;\;\defi\;\; \{ a \mapsto x, \ldots , b \mapsto y\}$		A
*	SIMP_CONVERSE_COMPSET	$\{ X \qdot P \mid x\mapsto y\} ^{-1} \;\;\defi\;\; \{ X \qdot P \mid y\mapsto x\}$		A
*	SIMP_DOM_ID	$\dom (\id) \;\;\defi\;\; S$	where $\id$ has type $\pow(S \cprod S)$	A
*	SIMP_RAN_ID	$\ran (\id) \;\;\defi\;\; S$	where $\id$ has type $\pow(S \cprod S)$	A
*	SIMP_FCOMP_ID_L	$(S \domres \id) \fcomp r \;\;\defi\;\; S \domres r$		A
*	SIMP_FCOMP_ID_R	$r \fcomp (S \domres \id) \;\;\defi\;\; r \ranres S$		A
*	SIMP_SPECIAL_REL_R	$S \rel \emptyset \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\srel \pfun \pinj \psur$	A
*	SIMP_SPECIAL_REL_L	$\emptyset \rel S \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\trel \pfun \tfun \pinj \tinj$	A
*	SIMP_FUNIMAGE_PRJ1	$\prjone (E \mapsto F) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_PRJ2	$\prjtwo (E \mapsto F) \;\;\defi\;\; F$		A
*	SIMP_DOM_PRJ1	$\dom (\prjone) \;\;\defi\;\; S \cprod T$	where $\prjone$ has type $\pow(S \cprod T \cprod S)$	A
*	SIMP_DOM_PRJ2	$\dom (\prjtwo) \;\;\defi\;\; S \cprod T$	where $\prjtwo$ has type $\pow(S \cprod T \cprod T)$	A
*	SIMP_RAN_PRJ1	$\ran (\prjone) \;\;\defi\;\; S$	where $\prjone$ has type $\pow(S \cprod T \cprod S)$	A
*	SIMP_RAN_PRJ2	$\ran (\prjtwo) \;\;\defi\;\; T$	where $\prjtwo$ has type $\pow(S \cprod T \cprod T)$	A
*	SIMP_FUNIMAGE_LAMBDA	$(\lambda x \qdot P(x) \mid E(x))(y) \;\;\defi\;\; E(y)$		A
*	SIMP_DOM_LAMBDA	$\dom(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid E\}$		A
*	SIMP_RAN_LAMBDA	$\ran(\{x\qdot P\mid E\mapsto F) \;\;\defi\;\; \{x\qdot P\mid F\}$		A
*	SIMP_IN_FUNIMAGE	$E\mapsto F(E)\in F \;\;\defi\;\; \btrue$		A
*	SIMP_IN_FUNIMAGE_CONVERSE_L	$F^{-1}(E)\mapsto E\in F \;\;\defi\;\; \btrue$		A
*	SIMP_IN_FUNIMAGE_CONVERSE_R	$F(E)\mapsto E\in F^{-1} \;\;\defi\;\; \btrue$		A
*	SIMP_MULTI_FUNIMAGE_SETENUM_LL	$\{ A \mapsto E, \ldots , B \mapsto E\} (x) \;\;\defi\;\; E$		A
*	SIMP_MULTI_FUNIMAGE_SETENUM_LR	$\{ E, \ldots , x \mapsto y, \ldots , F\} (x) \;\;\defi\;\; y$		A
*	SIMP_MULTI_FUNIMAGE_OVERL_SETENUM	$(r \ovl \ldots \ovl \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y$		A
*	SIMP_MULTI_FUNIMAGE_BUNION_SETENUM	$(r \bunion \ldots \bunion \{ E, \ldots , x \mapsto y, \ldots , F\} )(x) \;\;\defi\;\; y$		A
*	SIMP_FUNIMAGE_CPROD	$(S \cprod \{ F\} )(x) \;\;\defi\;\; F$		A
*	SIMP_FUNIMAGE_ID	$\id (x) \;\;\defi\;\; x$		A
*	SIMP_FUNIMAGE_FUNIMAGE_CONVERSE	$f(f^{-1} (E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_CONVERSE_FUNIMAGE	$f^{-1}(f(E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM	$\{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\; E$		A
*	SIMP_FUNIMAGE_DOMRES	$(E \domres F)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	SIMP_FUNIMAGE_DOMSUB	$(E \domsub F)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	SIMP_FUNIMAGE_RANRES	$(F\ranres E)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	SIMP_FUNIMAGE_RANSUB	$(F \ransub E)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	SIMP_FUNIMAGE_SETMINUS	$(F \setminus E)(G)\;\;\defi\;\;F(G)$	with hypothesis$F \in \mathit{A} \ \mathit{op}\ \mathit{B}$ where $\mathit{op}$ is one of $\pfun$, $\tfun$, $\pinj$, $\tinj$, $\psur$, $\tsur$, $\tbij$.	AM
*	DEF_EQUAL_FUNIMAGE	$f(x) = y \;\;\defi\;\; x \mapsto y \in f$		M
*	DEF_BCOMP	$r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r$		M
	DERIV_ID_SING	$\{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\}$	where $E$ is a single expression	M
*	SIMP_SPECIAL_DOM	$\dom (\emptyset ) \;\;\defi\;\; \emptyset$		A
*	SIMP_SPECIAL_RAN	$\ran (\emptyset ) \;\;\defi\;\; \emptyset$		A
*	SIMP_CONVERSE_CONVERSE	$r^{-1-1} \;\;\defi\;\; r$		A
*	DERIV_RELIMAGE_FCOMP	$(p \fcomp q)[s] \;\;\defi\;\; q[p[s]]$		M
*	DERIV_FCOMP_DOMRES	$(s \domres p) \fcomp q \;\;\defi\;\; s \domres (p \fcomp q)$		M
*	DERIV_FCOMP_DOMSUB	$(s \domsub p) \fcomp q \;\;\defi\;\; s \domsub (p \fcomp q)$		M
*	DERIV_FCOMP_RANRES	$p \fcomp (q \ranres s) \;\;\defi\;\; (p \fcomp q) \ranres s$		M
*	DERIV_FCOMP_RANSUB	$p \fcomp (q \ransub s) \;\;\defi\;\; (p \fcomp q) \ransub s$		M
	DERIV_FCOMP_SING	$\{E\mapsto F\}\fcomp\{F\mapsto G\} \;\;\defi\;\; \{E\mapsto G\}$		A
*	SIMP_SPECIAL_EQUAL_RELDOMRAN	$\emptyset \strel \emptyset \;\;\defi\;\; \{ \emptyset \}$	idem for operators $\tsur \tbij$	A
*	SIMP_TYPE_DOM	$\dom (\mathit{Ty}) \;\;\defi\;\; \mathit{Ta}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_TYPE_RAN	$\ran (\mathit{Ty}) \;\;\defi\;\; \mathit{Tb}$	where $\mathit{Ty}$ is a type expression equal to $\mathit{Ta} \cprod \mathit{Tb}$	A
*	SIMP_MULTI_DOM_CPROD	$\dom (E \cprod E) \;\;\defi\;\; E$		A
*	SIMP_MULTI_RAN_CPROD	$\ran (E \cprod E) \;\;\defi\;\; E$		A
*	SIMP_MULTI_DOM_DOMRES	$\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A$		A
*	SIMP_MULTI_DOM_DOMSUB	$\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A$		A
*	SIMP_MULTI_RAN_RANRES	$\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A$		A
*	SIMP_MULTI_RAN_RANSUB	$\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A$		A
*	DEF_IN_DOM	$E \in \dom (r) \;\;\defi\;\; \exists y \qdot E \mapsto y \in r$		M
*	DEF_IN_RAN	$F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r$		M
*	DEF_IN_CONVERSE	$E \mapsto F \in r^{-1} \;\;\defi\;\; F \mapsto E \in r$		M
*	DEF_IN_DOMRES	$E \mapsto F \in S \domres r \;\;\defi\;\; E \in S \land E \mapsto F \in r$		M
*	DEF_IN_RANRES	$E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \in T$		M
*	DEF_IN_DOMSUB	$E \mapsto F \in S \domsub r \;\;\defi\;\; E \notin S \land E \mapsto F \in r$		M
*	DEF_IN_RANSUB	$E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \notin T$		M
*	DEF_IN_RELIMAGE	$F \in r[w] \;\;\defi\;\; \exists x \qdot x \in w \land x \mapsto F \in r$		M
*	DEF_IN_FCOMP	$E \mapsto F \in (p \fcomp q) \;\;\defi\;\; \exists x \qdot E \mapsto x \in p \land x \mapsto F \in q$		M
*	DEF_OVERL	$p \ovl q \;\;\defi\;\; (\dom (q) \domsub p) \bunion q$		M
*	DEF_IN_ID	$E \mapsto F \in \id \;\;\defi\;\; E = F$		M
*	DEF_IN_DPROD	$E \mapsto (F \mapsto G) \in p \dprod q \;\;\defi\;\; E \mapsto F \in p \land E \mapsto G \in q$		M
*	DEF_IN_PPROD	$(E \mapsto G) \mapsto (F \mapsto H) \in p \pprod q \;\;\defi\;\; E \mapsto F \in p \land G \mapsto H \in q$		M
*	DEF_IN_REL	$r \in S \rel T \;\;\defi\;\; r\subseteq S\cprod T$		M
*	DEF_IN_RELDOM	$r \in S \trel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S$		M
*	DEF_IN_RELRAN	$r \in S \srel T \;\;\defi\;\; r \in S \rel T \land \ran (r) = T$		M
*	DEF_IN_RELDOMRAN	$r \in S \strel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S \land \ran (r) = T$		M
*	DEF_IN_FCT	$\begin{array}{rcl} f \in S \pfun T & \defi & f \in S \rel T \\ & \land & (\forall x,y,z \qdot x \mapsto y \in f \land x \mapsto z \in f \limp y = z) \\ \end{array}$		M
*	DEF_IN_TFCT	$f \in S \tfun T \;\;\defi\;\; f \in S \pfun T \land \dom (f) = S$		M
*	DEF_IN_INJ	$f \in S \pinj T \;\;\defi\;\; f \in S \pfun T \land f^{-1} \in T \pfun S$		M
*	DEF_IN_TINJ	$f \in S \tinj T \;\;\defi\;\; f \in S \pinj T \land \dom (f) = S$		M
*	DEF_IN_SURJ	$f \in S \psur T \;\;\defi\;\; f \in S \pfun T \land \ran (f) = T$		M
*	DEF_IN_TSURJ	$f \in S \tsur T \;\;\defi\;\; f \in S \psur T \land \dom (f) = S$		M
*	DEF_IN_BIJ	$f \in S \tbij T \;\;\defi\;\; f \in S \tinj T \land \ran (f) = T$		M
	DISTRI_BCOMP_BUNION	$r \bcomp (s \bunion t) \;\;\defi\;\; (r \bcomp s) \bunion (r \bcomp t)$		M
*	DISTRI_FCOMP_BUNION_R	$p \fcomp (q \bunion r) \;\;\defi\;\; (p \fcomp q) \bunion (p \fcomp r)$		M
*	DISTRI_FCOMP_BUNION_L	$(q \bunion r) \fcomp p \;\;\defi\;\; (q \fcomp p) \bunion (r \fcomp p)$		M
	DISTRI_DPROD_BUNION	$r \dprod (s \bunion t) \;\;\defi\;\; (r \dprod s) \bunion (r \dprod t)$		M
	DISTRI_DPROD_BINTER	$r \dprod (s \binter t) \;\;\defi\;\; (r \dprod s) \binter (r \dprod t)$		M
	DISTRI_DPROD_SETMINUS	$r \dprod (s \setminus t) \;\;\defi\;\; (r \dprod s) \setminus (r \dprod t)$		M
	DISTRI_DPROD_OVERL	$r \dprod (s \ovl t) \;\;\defi\;\; (r \dprod s) \ovl (r \dprod t)$		M
	DISTRI_PPROD_BUNION	$r \pprod (s \bunion t) \;\;\defi\;\; (r \pprod s) \bunion (r \pprod t)$		M
	DISTRI_PPROD_BINTER	$r \pprod (s \binter t) \;\;\defi\;\; (r \pprod s) \binter (r \pprod t)$		M
	DISTRI_PPROD_SETMINUS	$r \pprod (s \setminus t) \;\;\defi\;\; (r \pprod s) \setminus (r \pprod t)$		M
	DISTRI_PPROD_OVERL	$r \pprod (s \ovl t) \;\;\defi\;\; (r \pprod s) \ovl (r \pprod t)$		M
	DISTRI_OVERL_BUNION_L	$(p \bunion q) \ovl r \;\;\defi\;\; (p \ovl r) \bunion (q \ovl r)$		M
	DISTRI_OVERL_BINTER_L	$(p \binter q) \ovl r \;\;\defi\;\; (p \ovl r) \binter (q \ovl r)$		M
*	DISTRI_DOMRES_BUNION_R	$s \domres (p \bunion q) \;\;\defi\;\; (s \domres p) \bunion (s \domres q)$		M
*	DISTRI_DOMRES_BUNION_L	$(s \bunion t) \domres r \;\;\defi\;\; (s \domres r) \bunion (t \domres r)$		M
*	DISTRI_DOMRES_BINTER_R	$s \domres (p \binter q) \;\;\defi\;\; (s \domres p) \binter (s \domres q)$		M
*	DISTRI_DOMRES_BINTER_L	$(s \binter t) \domres r \;\;\defi\;\; (s \domres r) \binter (t \domres r)$		M
	DISTRI_DOMRES_SETMINUS_R	$s \domres (p \setminus q) \;\;\defi\;\; (s \domres p) \setminus (s \domres q)$		M
	DISTRI_DOMRES_SETMINUS_L	$(s \setminus t) \domres r \;\;\defi\;\; (s \domres r) \setminus (t \domres r)$		M
	DISTRI_DOMRES_DPROD	$s \domres (p \dprod q) \;\;\defi\;\; (s \domres p) \dprod (s \domres q)$		M
	DISTRI_DOMRES_OVERL	$s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (s \domres q)$		M
*	DISTRI_DOMSUB_BUNION_R	$s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q)$		M
*	DISTRI_DOMSUB_BUNION_L	$(s \bunion t) \domsub r \;\;\defi\;\; (s \domsub r) \binter (t \domsub r)$		M
*	DISTRI_DOMSUB_BINTER_R	$s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q)$		M
*	DISTRI_DOMSUB_BINTER_L	$(s \binter t) \domsub r \;\;\defi\;\; (s \domsub r) \bunion (t \domsub r)$		M
	DISTRI_DOMSUB_DPROD	$A \domsub (r \dprod s) \;\;\defi\;\; (A \domsub r) \dprod (A \domsub s)$		M
	DISTRI_DOMSUB_OVERL	$A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s)$		M
*	DISTRI_RANRES_BUNION_R	$r \ranres (s \bunion t) \;\;\defi\;\; (r \ranres s) \bunion (r \ranres t)$		M
*	DISTRI_RANRES_BUNION_L	$(p \bunion q) \ranres s \;\;\defi\;\; (p \ranres s) \bunion (q \ranres s)$		M
*	DISTRI_RANRES_BINTER_R	$r \ranres (s \binter t) \;\;\defi\;\; (r \ranres s) \binter (r \ranres t)$		M
*	DISTRI_RANRES_BINTER_L	$(p \binter q) \ranres s \;\;\defi\;\; (p \ranres s) \binter (q \ranres s)$		M
	DISTRI_RANRES_SETMINUS_R	$r \ranres (s \setminus t) \;\;\defi\;\; (r \ranres s) \setminus (r \ranres t)$		M
	DISTRI_RANRES_SETMINUS_L	$(p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s)$		M
*	DISTRI_RANSUB_BUNION_R	$r \ransub (s\bunion t) \;\;\defi\;\; (r \ransub s) \binter (r \ransub t)$		M
*	DISTRI_RANSUB_BUNION_L	$(p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s)$		M
*	DISTRI_RANSUB_BINTER_R	$r \ransub (s \binter t) \;\;\defi\;\; (r \ransub s) \bunion (r \ransub t)$		M
*	DISTRI_RANSUB_BINTER_L	$(p \binter q) \ransub s \;\;\defi\;\; (p \ransub s) \binter (q \ransub s)$		M
*	DISTRI_CONVERSE_BUNION	$(p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1}$		M
	DISTRI_CONVERSE_BINTER	$(p \binter q)^{-1} \;\;\defi\;\; p^{-1} \binter q^{-1}$		M
	DISTRI_CONVERSE_SETMINUS	$(r \setminus s)^{-1} \;\;\defi\;\; r^{-1} \setminus s^{-1}$		M
	DISTRI_CONVERSE_BCOMP	$(r \bcomp s)^{-1} \;\;\defi\;\; (s^{-1} \bcomp r^{-1} )$		M
	DISTRI_CONVERSE_FCOMP	$(p \fcomp q)^{-1} \;\;\defi\;\; (q^{-1} \fcomp p^{-1} )$		M
	DISTRI_CONVERSE_PPROD	$(r \pprod s)^{-1} \;\;\defi\;\; r^{-1} \pprod s^{-1}$		M
	DISTRI_CONVERSE_DOMRES	$(s \domres r)^{-1} \;\;\defi\;\; r^{-1} \ranres s$		M
	DISTRI_CONVERSE_DOMSUB	$(s \domsub r)^{-1} \;\;\defi\;\; r^{-1} \ransub s$		M
	DISTRI_CONVERSE_RANRES	$(r \ranres s)^{-1} \;\;\defi\;\; s \domres r^{-1}$		M
	DISTRI_CONVERSE_RANSUB	$(r \ransub s)^{-1} \;\;\defi\;\; s \domsub r^{-1}$		M
*	DISTRI_DOM_BUNION	$\dom (r \bunion s) \;\;\defi\;\; \dom (r) \bunion \dom (s)$		M
*	DISTRI_RAN_BUNION	$\ran (r \bunion s) \;\;\defi\;\; \ran (r) \bunion \ran (s)$		M
*	DISTRI_RELIMAGE_BUNION_R	$r[S \bunion T] \;\;\defi\;\; r[S] \bunion r[T]$		M
*	DISTRI_RELIMAGE_BUNION_L	$(p \bunion q)[S] \;\;\defi\;\; p[S] \bunion q[S]$		M
*	DERIV_DOM_TOTALREL	$\dom (r) \;\;\defi\;\; E$	with hypothesis $r \in E \ \mathit{op}\ F$, where $\mathit{op}$ is one of $\trel, \strel, \tfun, \tinj, \tsur, \tbij$	M
	DERIV_RAN_SURJREL	$\ran (r) \;\;\defi\;\; F$	with hypothesis $r \in E \ \mathit{op}\ F$, where $\mathit{op}$ is one of $\srel,\strel, \psur, \tsur, \tbij$	M
*	DERIV_PRJ1_SURJ	$\prjone \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue$	where $\mathit{Ty}_1$ and $\mathit{Ty}_2$ are types and $\mathit{op}$ is one of $\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur$	A
*	DERIV_PRJ2_SURJ	$\prjtwo \in\mathit{Ty}_1\ \mathit{op}\ \mathit{Ty}_2\;\;\defi\;\; \btrue$	where $\mathit{Ty}_1$ and $\mathit{Ty}_2$ are types and $\mathit{op}$ is one of $\rel, \trel, \srel, \strel, \pfun, \tfun, \psur, \tsur$	A
*	DERIV_ID_BIJ	$\id \in\mathit{Ty}\ \mathit{op}\ \mathit{Ty}\;\;\defi\;\; \btrue$	where $\mathit{Ty}$ is a type and $\mathit{op}$ is any arrow	A
*	SIMP_MAPSTO_PRJ1_PRJ2	$\prjone(E)\mapsto\prjtwo(E)\;\;\defi\;\; E$		A
	DERIV_EXPAND_PRJS	$E \;\;\defi\;\; \prjone(E) \mapsto \prjtwo(E)$		M
*	SIMP_DOM_SUCC	$\dom(\usucc) \;\;\defi\;\; \intg$		A
*	SIMP_RAN_SUCC	$\ran(\usucc) \;\;\defi\;\; \intg$		A
*	DERIV_MULTI_IN_BUNION	$E\in A\bunion\cdots\bunion\left\{\cdots, E,\cdots\right\}\bunion\cdots\bunion B\;\;\defi\;\; \btrue$		A
*	DERIV_MULTI_IN_SETMINUS	$E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse$		A
*	DEF_PRED	$\upred\;\;\defi\;\; \usucc^{-1}$		A
*	SIMP_SPECIAL_IN_ID	$E \mapsto E \in \id \;\;\defi\;\; \btrue$		A
*	SIMP_SPECIAL_IN_SETMINUS_ID	$E \mapsto E \in r \setminus \id \;\;\defi\;\; \bfalse$		A
*	SIMP_SPECIAL_IN_DOMRES_ID	$E \mapsto E \in S \domres \id \;\;\defi\;\; E \in S$		A
*	SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID	$E \mapsto E \in r \setminus (S \domres \id) \;\;\defi\;\; E \mapsto E \in S \domsub r$		A

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

Extension 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.

Rewrite Rules

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

Inference Rules

	Name	Rule	Side Condition	A/M
*	DATATYPE_DISTINCT_CASE	$\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} }$	where $x$ has a datatype $DT$ as type and appears free in $\textbf{G}$, $DT$ has constructors $c_1, \ldots, c_n$, parameters $p_{ij}$ are introduced as fresh identifiers	M
*	DATATYPE_INDUCTION	$\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) }$	where $x$ has inductive datatype $DT$ as type and appears free in $\textbf{P}$; $\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}$ are the inductive parameters (if any); an antecedent is created for every constructor $c_i$ of $DT$; all parameters are introduced as fresh identifiers; examples here	M