# Arithmetic Rewrite Rules

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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 $[itex]i = j[itex] \;\;\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 $[itex]i > j[itex] \;\;\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