Set Rewrite Rules

From Event-B
Jump to: navigation, search

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