Set Rewrite Rules

From Event-B
Revision as of 10:16, 11 May 2009 by imported>Nicolas
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
  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_OR   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_MULTI_EQV_NOT_NOT   \lnot\, P \leqv  \lnot\, P \;\;\defi\;\;  \btrue 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 A
* 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_FORALL   \forall \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \forall z \qdot  P(z) A
* SIMP_EXISTS   \exists \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \exists z \qdot  P(z) 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 M
* DERIV_SUBSETEQ_BINTER   S \subseteq  A \binter  \ldots  \binter  B \;\;\defi\;\;  S \subseteq  A \land  \ldots  \land  S \subseteq  B M
* SIMP_SUBSET_BUNION   A \bunion  \ldots  \bunion  B  \subset  S \;\;\defi\;\;  A  \subset  S \land  \ldots  \land  B  \subset  S A
* SIMP_SUBSET_BINTER   S  \subset  A \binter  \ldots  \binter  B \;\;\defi\;\;  S  \subset  A \land  \ldots  \land  S  \subset  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  \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\;\;  S 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_TYPE_KUNION   \union (\mathit{Ty}) \;\;\defi\;\;  \mathit{Ta} where \mathit{Ty} is a type expression and \mathit{Ty} = \pow (\mathit{Ta}) 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_TYPE_KINTER   \inter (\mathit{Ty}) \;\;\defi\;\;  \emptyset where \mathit{Ty} is a type expression 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 \qdot  x = E \mid  x \}  \;\;\defi\;\;  \{ E\} where x non free in E A
* SIMP_COMPSET_IN   \{  x \qdot  x \in  S \mid  x \}  \;\;\defi\;\;  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  x \}  \;\;\defi\;\;  \mathit{Ty} where the type od x is \mathit{Ty} A
* SIMP_SUBSETEQ_COMPSET_L   \{  x \qdot  P(x) \mid  E \}  \subseteq  S \;\;\defi\;\;  \forall x\qdot  P(x) \limp  E \in  S where x non free in S A
SIMP_SPECIAL_EQUAL_COMPSET   \{  x \qdot  P(x) \mid  E \}  = \emptyset  \;\;\defi\;\;  \forall x\qdot  \lnot\, P(x) A
* SIMP_IN_COMPSET   E \in  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  P(E) 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 x, S, \{  x \qdot  P(x) \mid  x \} A
SIMP_SPECIAL_OVERL   r \ovl  \ldots  \ovl  \emptyset  \ovl  \ldots  \ovl  s \;\;\defi\;\;  r \ovl  \ldots  \ovl  s A
* SIMP_MULTI_OVERL \begin{array}{cl} & r \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  u \\ \defi &  r \ovl  \ldots  \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  u \end{array} A
* SIMP_TYPE_OVERL_CPROD   r \ovl  (\mathit{Ty} \cprod  S) \;\;\defi\;\;  (\mathit{Ty} \cprod  S) where \mathit{Ty} is a type expression 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 n\in\nat\land 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_BINTER_L   \finite (S \binter  T) \;\;\defi\;\;  \finite (S) M
* SIMP_FINITE_BINTER_R   \finite (S \binter  T) \;\;\defi\;\;  \finite (T) M
* SIMP_FINITE_SETMINUS   \finite (S \setminus T) \;\;\defi\;\;  \finite (S) M
* SIMP_FINITE_DOMRES   \finite (S \domres  r)  \;\;\defi\;\;  \finite (r) M
* SIMP_FINITE_RANRES   \finite (r \ranres  S)  \;\;\defi\;\;  \finite (r) M
* SIMP_FINITE_DOMSUB   \finite (S \domsub  r) \;\;\defi\;\;  \finite (r) M
* SIMP_FINITE_RANSUB   \finite (r \ransub  S) \;\;\defi\;\;  \finite (r) M
* SIMP_FINITE_RELIMAGE   \finite (r[S]) \;\;\defi\;\;  \finite (r) M
* SIMP_FINITE_CPROD   \finite (S \cprod  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) M
* SIMP_FINITE_OVERL   \finite (r \ovl  s)  \;\;\defi\;\;  \finite (r) \land  \finite (s) M
* SIMP_FINITE_REL   \finite (S \rel  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) M
* SIMP_FINITE_FCOMP   \finite (r \fcomp s) \;\;\defi\;\;  \finite (r) \land  \finite (s) M
* SIMP_FINITE_BCOMP   \finite (r \bcomp  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) M
* SIMP_FINITE_DPROD   \finite (r \dprod  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) M
* SIMP_FINITE_PPROD   \finite (r \pprod  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) M
* SIMP_FINITE_COMPSET   \finite (\{ x \qdot  x \in  S \land  \ldots  \land  P \mid  x\} ) \;\;\defi\;\;  \finite (S) where x non free in S M
* SIMP_FINITE_RAN   \finite (\ran (r)) \;\;\defi\;\;  \finite (r) M
* SIMP_FINITE_DOM   \finite (\dom (r)) \;\;\defi\;\;  \finite (r) M
* SIMP_FINITE_QUNION   \finite (\Union  x \qdot  P \mid  E) \;\;\defi\;\;  \forall x \qdot  P \limp  \finite (E) M
* SIMP_FINITE_QINTER   \finite (\Inter  x \qdot  P \mid  E) \;\;\defi\;\;  \exists x \qdot  P \land  \finite (E) M
* SIMP_FINITE_ID   \finite (\id (S)) \;\;\defi\;\;  \finite (S) 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_LAMBDA   \finite (\lambda x \qdot  P \mid  E) \;\;\defi\;\;  \finite (\{ x \qdot  P \mid  x\} ) A
* SIMP_TYPE_EQUAL_EMPTY  \mathit{Ty} = \emptyset  \;\;\defi\;\;  \bfalse where \mathit{Ty} is a type expression A
* SIMP_TYPE_IN   t \in  \mathit{Ty} \;\;\defi\;\;  \btrue where \mathit{Ty} is a type expression A
SIMP_SPECIAL_FORALL_BTRUE   \forall x \qdot  \btrue  \;\;\defi\;\;  \btrue A
SIMP_SPECIAL_FORALL_BFALSE   \forall x \qdot  \bfalse  \;\;\defi\;\;  \bfalse A
SIMP_SPECIAL_EXISTS_BTRUE   \exists x \qdot  \btrue  \;\;\defi\;\;  \btrue A
SIMP_SPECIAL_EXISTS_BFALSE   \exists x \qdot  \bfalse  \;\;\defi\;\;  \bfalse A
* SIMP_SPECIAL_EQV_BTRUE   P \leqv  \btrue  \;\;\defi\;\;  P A
* SIMP_SPECIAL_EQV_BFALSE   P \leqv  \bfalse  \;\;\defi\;\;  \lnot\, P A
SIMP_SPECIAL_SUBSET_R   S  \subset  \emptyset  \;\;\defi\;\;  \bfalse A
SIMP_SPECIAL_SUBSET_L   \emptyset   \subset  S \;\;\defi\;\;  S \neq  \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
* 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 \limp  \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_SPECIAL_NOT_EQUAL   \lnot\, S = \emptyset  \;\;\defi\;\;  \exists x \qdot  x \in  S M
* DEF_IN_MAPSTO   E \mapsto  F \in  S \cprod  T \;\;\defi\;\;  E \in  S \land  F \in  T M
* DEF_IN_POW   E \in  \pow (S) \;\;\defi\;\;  E \subseteq  S M
* DEF_SUBSETEQ   \forall x \qdot  x \in  S \limp  x \in  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 M
* DEF_IN_QUNION   E \in  (\Union  x \qdot  x \in  S \land  P \mid  T) \;\;\defi\;\;  \exists x \qdot  x \in  S \land  P \land  E \in  T M
* DEF_IN_KINTER   E \in  \inter (S) \;\;\defi\;\;  \forall s \qdot  s \in  S \limp  E \in  s M
* DEF_IN_QINTER   E \in  (\Inter  x \qdot  x \in  S \land  P \mid  T) \;\;\defi\;\;  \forall x \qdot  x \in  S \land  P \limp  E \in  T 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^n, s_2^n, \ldots, s_n^n) \;\;\defi\;\; 
 		  	\begin{array}{l}
		  		s = s_1\bunion s_2\bunion\cdots\bunion s_n\\
				s_1\binter s_2 = \emptyset\\
				\vdots\\
				s_1\binter s_n = \emptyset\\
				\vdots\\
				s_{n-1}\binter s_n = \emptyset\\
			\end{array} AM