Arithmetic Rewrite Rules

	Name	Rule	Side Condition	A/M
SIMP_SPECIAL_MOD_0	$0 \,\bmod\, E \;\;\defi\;\; 0$		A
SIMP_SPECIAL_MOD_1	$E \mod 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_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_LIT_MIN_UPTO	$\min (\{ i, \ldots , j\} ) \;\;\defi\;\; A \;\;(computation)$	where $i, ... ,\,j$ are literals	A
SIMP_LIT_MAX_UPTO	$\max (\{ i, \ldots , j\} ) \;\;\defi\;\; A \;\;(computation)$	where $i, ... ,\,j$ are literals	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 ^ \card (S)$		A
SIMP_CARD_BUNION	$\card (S \bunion T) \;\;\defi\;\; \card (S) + \card (T) - \card (S \binter T)$		A
SIMP_CARD_CONVERSE	$\card (r^{-1} ) \;\;\defi\;\; \card (r)$		A
SIMP_CARD_ID	$\card (\id (S)) \;\;\defi\;\; \card (S)$		A
SIMP_CARD_LAMBDA	$\card (\lambda x\qdot (P \mid E)) \;\;\defi\;\; \card (\{ x \qdot P \mid x\} )$		A
SIMP_CARD_COMPSET	$\card (\{ x \qdot x \in S \mid x\} ) \;\;\defi\;\; \card (S)$	where $x$ non free in $S$	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_0	$\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 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 literal and $1 \leq i$	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 literal and $1 \leq i$	A
SIMP_LIT_IN_MINUS_NATURAL1	$-i \in \natn \;\;\defi\;\; \bfalse$	where $i$ is a literal	A
SIMP_SPECIAL_KBOOL_BTRUE	$\bool (\btrue ) \;\;\defi\;\; \True$		A
SIMP_SPECIAL_KBOOL_BFALSE	$\bool (\bfalse ) \;\;\defi\;\; \False$		A
SIMP_LIT_EQUAL_KBOOL_TRUE	$\bool (P) = \True \;\;\defi\;\; P$		A
SIMP_LIT_EQUAL_KBOOL_FALSE	$\bool (P) = \False \;\;\defi\;\; \lnot\, P$		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_MULTI_MINUS	$E - E \;\;\defi\;\; 0$		A
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_MINUS_MINUS	$- (-i) \;\;\defi\;\; i$	where $i$ is a literal	A
SIMP_LIT_EQUAL	$<math>i = j<math> \;\;\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	$<math>i > j<math> \;\;\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	$E ^ 1 \;\;\defi\;\; E$		A
SIMP_SPECIAL_EXPN_0	$E ^ 0 \;\;\defi\;\; 1$		A
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_MOD	$E \mod 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_LE_CARD	$\card (S) \leq \card (T) \;\;\defi\;\; S \subseteq T$	$S$ and $T$ must be of the same type	M
DERIV_GE_CARD	$\card (S) \geq \card (T) \;\;\defi\;\; T \subseteq S$	$S$ and $T$ must be of the same type	M
DERIV_LT_CARD	$\card (S) < \card (T) \;\;\defi\;\; S \subset T$	$S$ and $T$ must be of the same type	M
DERIV_GT_CARD	$\card (S) > \card (T) \;\;\defi\;\; T \subset S$	$S$ and $T$ must be of the same type	M
DERIV_EQUAL_CARD	$\card (S) = \card (T) \;\;\defi\;\; S = T$	$S$ and $T$ must be of the same type	M

Some rules are not yet implemented:

• SIMP_SPECIAL_KUNION, SIMP_SPECIAL_KUNION, SIMP_SPECIAL_KINTER, SIMP_SPECIAL_POW, SIMP_SPECIAL_POW1, SIMP_SPECIAL_CPROD_R, SIMP_SPECIAL_CPROD_L, SIMP_SPECIAL_COMPSET_BFALSE, SIMP_SPECIAL_COMPSET_BTRUE, SIMP_SPECIAL_EQUAL_COMPSET, SIMP_SPECIAL_OVERL, SIMP_SPECIAL_DOMRES_L, SIMP_SPECIAL_DOMRES_R, SIMP_SPECIAL_RANRES_R, SIMP_SPECIAL_RANRES_L, SIMP_SPECIAL_DOMSUB_L, SIMP_SPECIAL_DOMSUB_R, SIMP_SPECIAL_RANSUB_R, SIMP_SPECIAL_RANSUB_L, SIMP_SPECIAL_FCOMP, SIMP_SPECIAL_BCOMP, SIMP_SPECIAL_DPROD_R, SIMP_SPECIAL_DPROD_L, SIMP_SPECIAL_PPROD_R, SIMP_SPECIAL_PPROD_L, SIMP_SPECIAL_RELIMAGE_L, SIMP_SPECIAL_CONVERSE, SIMP_SPECIAL_ID, SIMP_SPECIAL_REL_R, SIMP_SPECIAL_REL_L, SIMP_SPECIAL_EQUAL_REL, SIMP_SPECIAL_EQUAL_RELDOM, SIMP_SPECIAL_PRJ1, SIMP_SPECIAL_PRJ2, SIMP_SPECIAL_LAMBDA, SIMP_SPECIAL_MOD_0, SIMP_SPECIAL_MOD_1, SIMP_SPECIAL_IN_NATURAL1, SIMP_SPECIAL_KBOOL_BTRUE, SIMP_SPECIAL_KBOOL_BFALSE, SIMP_SPECIAL_DIV_1, SIMP_SPECIAL_EQUAL_RELDOMRAN, SIMP_SPECIAL_FORALL_BTRUE, SIMP_SPECIAL_FORALL_BFALSE, SIMP_SPECIAL_EXIST_BTRUE, SIMP_SPECIAL_EXIST_BFALSE, SIMP_SPECIAL_SUBSET_R, SIMP_SPECIAL_SUBSET_L